We describe a first order axiom set which yields the classical first order Euclidean geometry of Tarski when used with classical logic, and yields an intuitionistic Euclidean geometry when used with intuitionistic logic. The first order language has a single six place atomic predicate and no function symbols. The intuitionistic system has a computational interpretation in recursive function theory, that is, a realizability interpretation analogous to those given by Kleene for intuitionistic arithmetic and analysis. This interpretation shows the unprovability in (...) the intuitionistic theory of certain “nonconstructive” theorems of the classical geometry. (shrink)

Though pictures are often used to present mathematical arguments, they are not typically thought to be an acceptable means for presenting mathematical arguments rigorously. With respect to the proofs in the Elements in particular, the received view is that Euclid's reliance on geometric diagrams undermines his efforts to develop a gap-free deductive theory. The central difficulty concerns the generality of the theory. How can inferences made from a particular diagrams license general mathematical results? After surveying the history behind the received (...) view, this essay provides a contrary analysis by introducing a formal account of Euclid's proofs, termed Eu. Eu solves the puzzle of generality surrounding Euclid's arguments. It specifies what diagrams Euclid's diagrams are, in a precise formal sense, and defines generality-preserving proof rules in terms of them. After the central principles behind the formalization are laid out, its implications with respect to the question of what does and does not constitute a genuine picture proof are explored. (shrink)

This chapter gives a detailed study of diagram-based reasoning in Euclidean plane geometry (Books I, III), as well as an exploration how to characterise a geometric practice. First, an account is given of diagram attribution: basic geometrical claims are classified as exact (equalities, proportionalities) or co-exact (containments, contiguities); exact claims may only be inferred from prior entries in the demonstration text, but co-exact claims may be asserted based on what is seen in the diagram. Diagram control by constructions is necessary (...) for this to work. Case-branching occurs when a construction renders a diagram un-representative. The roles of diagrams in reductio arguments, and of objection in probing a demonstration, are discussed. (shrink)

We review and contrast three ways to make up a formal Euclidean geometry which one might call constructive, in a computational sense. The starting point is the first-order geometry created by Tarski.

We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning.

A survey of Euclid's Elements, this text provides an understanding of the classical Greek conception of mathematics and its similarities to modern views as well as its differences. It focuses on philosophical, foundational, and logical questions — rather than strictly historical and mathematical issues — and features several helpful appendixes.

The material contained in the following translation was given in substance by Professor Hilbertas a course of lectures on euclidean geometry at the University of G]ottingen during the wintersemester of 1898-1899. The results of his investigation were re-arranged and put into the formin which they appear here as a memorial address published in connection with the celebration atthe unveiling of the Gauss-Weber monument at G]ottingen, in June, 1899. In the French edition, which appeared soon after, Professor Hilbert made some additions, (...) particularly in the concludingremarks, where he gave an account of the results of a recent investigation made by Dr. Dehn.These additions have been incorporated in the following translation.Geometry, like arithmetic, requires for its logical development only a small number ofsimple, fundamental principles. These fundamental principles are called the axioms ofgeometry. The choice of the axioms and the investigation of their relations to one anotheris a problem which, since the time of Euclid, has been discussed in numerous excellentmemoirs to be found in the mathematical literature.1 This problem is tantamount to thelogical analysis of our intuition of space. (shrink)

Moritz Pasch (1843ber neuere Geometrie (1882), in which he also clearly formulated the view that deductions must be independent from the meanings of the nonlogical terms involved. Pasch also presented in these lectures the main tenets of his philosophy of mathematics, which he continued to elaborate on throughout the rest of his life. This philosophy is quite unique in combining a deductivist methodology with a radically empiricist epistemology for mathematics. By taking into consideration publications from the entire span of Paschs (...) highly original, but virtually unknown, philosophy of mathematics is presented. (shrink)

Three things are presented: How Hilbert changed the original construction postulates of his geometry into existential axioms; In what sense he formalized geometry; How elementary geometry is formalized to present day's standards.

Three things are presented: How Hilbert changed the original construction postulates of his geometry into existential axioms; In what sense he formalized geometry; How elementary geometry is formalized to present day's standards.

Elementary geometry can be axiomatized constructively by taking as primitive the concepts of the apartness of a point from a line and the convergence of two lines, instead of incidence and parallelism as in the classical axiomatizations. I first give the axioms of a general plane geometry of apartness and convergence. Constructive projective geometry is obtained by adding the principle that any two distinct lines converge, and affine geometry by adding a parallel line construction, etc. Constructive axiomatization allows solutions to (...) geometric problems to be effected as computer programs. I present a formalization of the axiomatization in type theory. This formalization works directly as a computer implementation of geometry. (shrink)