In this paper we provide quantifier-free, constructive axiomatizations for 2-dimensional absolute, Euclidean, and hyperbolic geometry. The main novelty consists in the first-order languages in which the axiom systems are formulated.

We provide a universal axiom system for plane hyperbolic geometry in a firstorder language with two sorts of individual variables, ‘points’ and ‘lines’ , containing three individual constants, A0, A1, A2, standing for three non-collinear points, two binary operation symbols, φ and ι, with φ = l to be interpreted as ‘[MATHEMATICAL SCRIPT SMALL L] is the line joining A and B’ , and ι = P to be interpreted as [MATHEMATICAL SCRIPT SMALL L]P is the point of (...) intersection of g and h , and two binary operation symbols, π1 and —2, with πi = g to be interpreted as ‘g is one of the two limiting paralle lines from P to [MATHEMATICAL SCRIPT SMALL L]. (shrink)

H. Tietze has proved algebraically that the geometry of uniquely determined ruler and compass constructions coincides with the geometry of ruler and set square constructions. We provide a new proof of this result via new universal axiom systems for Euclidean planes of characteristic ≠ 2 in languages containing only operation symbols.

This paper continues the investigations begun in [6] and continued in [7] about quantifier-free axiomatizations of plane Euclidean geometry using ternary operations. We show that plane Euclidean geometry over Archimedean ordered Euclidean fields can be axiomatized using only two ternary operations if one allows axioms that are not first-order but universal Lw1,w sentences. The operations are: the transport of a segment on a halfline that starts at one of the endpoints of the given segment, and the (...) operation which produces one of the intersection points of a perpendicular on a diameter of a circle with that circle. MSC: 03F65, 51M05, 51M15. (shrink)

We proved in the first part [1] that plane geometry over Pythagorean fields is axiomatizable by quantifier-free axioms in a language with three individual constants, one binary and three ternary operation symbols. In this paper we prove that two of these operation symbols are superfluous.

In this paper we provide quantifier-free, constructive axiomatizations for several fragments of plane Euclidean geometry over Euclidean fields, such that each axiom contains at most 4 variables. The languages in which they are expressed contain only at most ternary operations. In some precisely defined sense these axiomatizations are the simplest possible.

In this paper we provide a quantifier-free, constructive axiomatization of metric-Euclidean and of rectangular planes . The languages in which the axiom systems are expressed contain three individual constants and two ternary operations. We also provide an axiom system in algorithmic logic for finite Euclidean planes, and for several minimal metric-Euclidean planes. The axiom systems proposed will be used in a sequel to this paper to provide ‘the simplest possible’ axiom systems for several fragments of plane Euclidean (...) class='Hi'>geometry. (shrink)

In this paper we provide a quantifier-free constructive axiomatization for Euclidean planes in a first-order language with only ternary operation symbols and three constant symbols . We also determine the algorithmic theories of some ‘naturally occurring’ plane geometries.

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)

This paper provides a detailed study of David Hilbert’s axiomatization of the theory of plane area, in the classical monograph Foundation of Geometry. On the one hand, we offer a precise contextualization of this theory by considering it against its nineteenth-century geometrical background. Specifically, we examine some crucial steps in the emergence of the modern theory of geometrical equivalence. On the other hand, we analyze from a more conceptual perspective the significance of Hilbert’s theory of area for (...) the foundational program pursued in Foundations. We argue that this theory played a fundamental role in the general attempt to provide a new independent basis for Euclidean geometry. Furthermore, we contend that our examination proves relevant for understanding the requirement of “purity of the method” in the tradition of modern synthetic geometry. (shrink)

Hyperbolic geometry can be axiomatized using the notions of order andcongruence (as in Euclidean geometry) or using the notion of incidencealone (as in projective geometry). Although the incidence-based axiomatizationmay be considered simpler because it uses the single binary point-linerelation of incidence as a primitive notion, we show that it issyntactically more complex. The incidence-based formulation requires some axioms of the quantifier-type \forall\exists\forall, while the axiom system based on congruence and order can beformulated using only \forall\exists-axioms.

Hyperbolic geometry can be axiomatized using the notions of order andcongruence (as in Euclidean geometry) or using the notion of incidencealone (as in projective geometry). Although the incidence-based axiomatizationmay be considered simpler because it uses the single binary point-linerelation of incidence as a primitive notion, we show that it issyntactically more complex. The incidence-based formulation requires some axioms of the quantifier-type forallexistsforall, while the axiom system based on congruence and order can beformulated using only forallexists-axioms.

Minkowski geometry is axiomatized in terms of the asymmetric binary relation of optical connectibility, using ten first-order axioms and the second-order continuity axiom. An axiom system in terms of the symmetric binary optical connection relation is also presented. The present development is much simpler than the corresponding work of Robb, upon which it is modeled.

Proposition I.1 is, by far, the most popular example used to justify the thesis that many of Euclid’s geometric arguments are diagram-based. Many scholars have recently articulated this thesis in different ways and argued for it. My purpose is to reformulate it in a quite general way, by describing what I take to be the twofold role that diagrams play in Euclid’s plane geometry (EPG). Euclid’s arguments are object-dependent. They are about geometric objects. Hence, they cannot be diagram-based (...) unless diagrams are supposed to have an appropriate relation with these objects. I take this relation to be a quite peculiar sort of representation. Its peculiarity depends on the two following claims that I shall argue for: ( i ) The identity conditions of EPG objects are provided by the identity conditions of the diagrams that represent them; ( ii ) EPG objects inherit some properties and relations from these diagrams. (shrink)

We show that plane hyperbolic geometry, expressed in terms of points and the ternary relation of collinearity alone, cannot be expressed by means of axioms of complexity at most ∀∃∀, but that there is an axiom system, all of whose axioms are ∀∃∀∃ sentences. This remains true for Klingenberg's generalized hyperbolic planes, with arbitrary ordered fields as coordinate fields.

Inquiries of Wellstein, Grünbaum and others have proved that there are indefinitely many different spatial models of Euklidian geometry. The points, lines and planes of these models are related to each other as the points, straight lines and planes of Euklidian geometry, but they are obviously totally different from them. That means that the axiomatic Euklidian geometry does not clearly determine the spatial forms of their planes and straight lines. The constructive geometry basing on approaches of (...) Hugo Dingler tries to solve this problem of disambiguity so that a clear realization of the geometrical basic objects plane, straight line and rectangle and others is possible because of certain rules. On the one hand these rules are to pledge the techniques of realisation and on the other hand they are the basic for the deduction of statements on the technically realized geometrical basic objects. The rules are especially to pledge the selection of apt material that keep its form. The following will show that the disambiguity cannot be pledged by the mere laws established by the constructive geometry and especially that the problem of electing the material cannot be solved by these laws. Furthermore it proves to be necessary to analyze and reconstruct more circumstances describing the selection of apt material which exceed the present standard of constructive geometry. (shrink)

In the 1920s Heyting attempted at axiomatizing constructive geometry. Recently, von Plato used different concepts to axiomatize it. He used 14 axioms to formulate constructive apartness geometry, seven of which have occurrences of negation. In this paper we show with the help of ANDP, a theorem prover based on natural deduction, that four new axioms without negation, shorter and more intuitive, can replace seven of von Plato's 14 ones. Thus we obtained a near negation-free new system consisting of (...) 11 axioms. (shrink)

We show that the first-order theory of a large class of plane geometries and the first-order theory of their groups of motions, understood both as groups with a unary predicate singling out line-reflections, and as groups acting on sets, are mutually inter-pretable.

Peano's axiomatizations of geometry are abstract and non-intuitive in character, whereas Peano stresses his appeal to concrete spatial intuition in the choice of the axioms. This poses the problem of understanding the interrelationship between abstraction and intuition in his geometrical works. In this article I argue that axiomatization is, for Peano, a methodology to restructure geometry and isolate its organizing principles. The restructuring produces a more abstract presentation of geometry, which does not contradict its intuitive content (...) but only puts it into a particular form. (shrink)

Since the application of Postulate I.2 in Euclid's Elements is not uniform, one could wonder in what way should it be applied in Euclid's plane geometry. Besides legitimizing questions like this from the perspective of a philosophy of mathematical practice, we sketch a general perspective of conceptual analysis of mathematical texts, which involves an extended notion of mathematical theory as system of authorizations, and an audience-dependent notion of proof.

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)

Since the application of Postulate I.2 in Euclid’s Elements is not uniform, one could wonder in what way should it be applied in Euclid’s plane geometry. Besides legitimizing questions like this from the perspective of a philosophy of mathematical practice, we sketch a general perspective of conceptual analysis of mathematical texts, which involves an extended notion of mathematical theory as system of authorizations, and an audience-dependent notion of proof.

The standard coordinate-based formulation of the space-time theory of special relativity (Minkowski geometry) is philosophically unsatisfactory for various reasons. We here present an explicit axiomatic formulation of that theory in terms of primitives with a definitive physical interpretation, prove its equivalence to the standard coordinate formulation, and draw various philosophical conclusions concerning the physical content and assumptions of the space-time theory. The prevalent causal interpretation of physical Minkowski geometry deriving from Reichenbach is criticised on the basis of the (...) present formulation. (shrink)

In this paper, we discuss a proposal for reform in the teaching of Euclidean geometry that reveals the symbiotic relationship between axiomatics and pedagogy. We examine the role of intuition in this kind of reform, as expressed by Mario Pieri, a prominent member of the Schools of Peano and Segre at the University of Turin. We are well aware of the centuries of attention paid to the notion of intuition by mathematicians, mathematics educators, philosophers, psychologists, historians, and others. To (...) set a context for Pieri’s proposal, we only seek to open a small window on views of the pedagogical role of intuition, from primary education to university study that may have informed early 20th century efforts to improve the teaching of geometry at the secondary school level. Pieri addressed the topic of intuition in many of his axiomatizations, including those in projective geometry which was his main area of concentration in foundations. We focus here primarily on his axiom systems for elementary geometry, which embraced the transformational approach of Felix Klein’s vision for the subject. Our goal is to convey Pieri’s thoughts on how to integrate two types of intuition, denoted as sensible and rational, in his endeavors to improve the teaching of the geometry of Euclid. We show how Pieri’s views on geometric intuition and pedagogical reform were either ignored or misrepresented in several notable publications at the turn of the 20th century. In particular, we give Pieri a voice in response to specific comments made in the early 1900s by Federigo Enriques, Ugo Amaldi, and Florian Cajori in widely circulated publications inspired by Klein. (shrink)

E. Beltrami in 1868 did not intend to prove the consistency of non-euclidean plane geometry nor the independence of the euclidean parallel postulate. His approach would have been unsuccessful if so intended. J. Hoüel in 1870 described the relevance of Beltrami's work to the issue of the independence of the euclidean parallel postulate. Hoüel's method is different from the independence proofs using reinterpretation of terms deployed by Peano about 1890, chiefly in using a fixed interpretation for non-logical terms. (...) Comparing the work of Beltrami and Hoüel with the treatment of non-euclidean geometry after the development of the axiomatic method in the 1890s indicates an important shift in mathematicians? attitudes towards mathematical theories. (shrink)

It is commonplace to view the rigor of the mathematics in Euclid's Elements in the way an experienced teacher views the work of an earnest beginner: respectable relative to an early stage of development, but ultimately flawed. Given the close connection in content between Euclid's Elements and high-school geometry classes, this is understandable. Euclid, it seems, never realized what everyone who moves beyond elementary geometry into more advanced mathematics is now customarily taught: a fully rigorous proof cannot rely (...) on geometric intuition. In his arguments he seems to call illicitly upon our understanding of how objects like triangles and circles behave rather than grounding everything rigorously in axioms.Though widespread, the attitude is in a historical sense puzzling. For over two millenia, mathematicians of all levels studied the arguments in Elements and found nothing substantial missing. The book, on the contrary, represented the limit of mathematical explicitness. It served as the paradigm for careful and exact reasoning. How it could enjoy this reputation for so long is mysterious if careful and exact reasoning demands that all inferences be grounded in a modern axiomatic theory in the way Hilbert did in his famous Foundations of Geometry. By these standards, Euclid's work is deeply flawed. The holes in his arguments are not minor and excusable, but massive and cryptic.With his book Euclid and His Twentieth Century Rivals, Nathaniel Miller makes substantial progress in clearing this mystery up. The book is an explication of FG , a formal system of proof developed by Miller which reconstructs Euclid's deductions as essentially diagrammatic. The holes in Euclid's arguments are taken to appear precisely at those steps which are unintelligible without an accompanying geometric diagram. Interpreting the reasoning in the Elements in terms of a modern axiomatization , …. (shrink)

Traditional geometry concerns itself with planimetric and stereometric considerations, which are at the root of the division between plane and solid geometry. To raise the issue of the relation between these two areas brings with it a host of different problems that pertain to mathematical practice, epistemology, semantics, ontology, methodology, and logic. In addition, issues of psychology and pedagogy are also important here. To our knowledge there is no single contribution that studies in detail even one of (...) the aforementioned areas. (shrink)

In this paper, I reconstruct Edmund Husserl's view on the relationship between formal inquiry and the life-world, using the example of formal geometry. I first outline Husserl's account of geometry and then argue that he believed that the applicability of formal geometry to intuitive space (the space of everyday-experience) guarantees the conceptual continuity between different notions of space.

We give a general account of the goals of axiomatization, introducing a variant on Detlefsen’s notion of ‘complete descriptive axiomatization’. We describe how distinctions between the Greek and modern view of number, magnitude, and proportion impact the interpretation of Hilbert’s axiomatization of geometry. We argue, as did Hilbert, that Euclid’s propositions concerning polygons, area, and similar triangles are derivable from Hilbert’s first-order axioms. We argue that Hilbert’s axioms including continuity show much more than the geometrical propositions (...) of Euclid’s theorems and thus are an immodest complete descriptive axiomatization of that subject. (shrink)

The paper outlines an interpretation of one of the most important and original contributions of David Hilbert’s monograph Foundations of Geometry , namely his internal arithmetization of geometry. It is claimed that Hilbert’s profound interest in the problem of the introduction of numbers into geometry responded to certain epistemological aims and methodological concerns that were fundamental to his early axiomatic investigations into the foundations of elementary geometry. In particular, it is shown that a central concern that (...) motivated Hilbert’s axiomatic investigations from very early on was the aim of providing an independent basis for geometry. Accordingly, these concerns about an independent grounding for elementary geometry determined very clear methodological constraints in the process of embedding it into a formal axiomatic system. It is argued that Hilbert not only sought to show that geometry could be considered a pure mathematical theory, once it was presented as a formal axiomatic system; he also aimed at showing that in the construction of such an axiomatic system one could proceed purely geometrically, avoiding concept formations borrowed from other mathematical disciplines like arithmetic or analysis. (shrink)

This book is a wonderful resource for historians and philosophers of mathematics and physics alike, not just for Hilbert's own work in physics, but also because Corry sets Hilbert in context, bringing out the people with whom Hilbert had contact, describing their work and possible links with Hilbert's work, and describing the activities going on around Hilbert. The historical thesis of this book is that Hilbert worked on a wide range of issues in physics for a period lasting more than (...) two decades, employing and developing his axiomatic approach throughout. One conclusion that follows from this is that Hilbert's 1915–1917 work relating to Einstein's General Theory of Relativity was a natural continuation of Hilbert's pre-existing interests and activities, and not a one-off foray into foreign territory. 1Of especial interest to philosophers of mathematics are two further theses. Corry stresses that for Hilbert geometry is an empirical science, and related to this argues first, that Hilbert intends the axiomatic method to be used in enhancing our understanding of the content of a given theory via relating the results of the axiomatic investigation back to the intuitive content of the axioms; and, second, that to understand Hilbert's axiomatic approach in mathematics we must pay serious attention to his work in physics.Corry also hopes to show ‘the significant and unique contribution of Hilbert to certain important developments in twentieth-century physics’ . 2 In the end, this assessment of Hilbert's contribution to physics is far from clear cut: the two cases where Hilbert goes into the details of a physical theory show him lacking feel for what is important physically with respect to that theory. Nevertheless, philosophers and historians of physics will find a great deal to interest them in the story of Hilbert's involvement in physics, and in the details …. (shrink)

Ken Pledger devised a one-sorted approach to the incidence relation of plane geometries, using structures that also support models of propositional modal logic. He introduced a modal system 12g that is valid in one-sorted projective planes, proved that it has finitely many non-equivalent modalities, and identified all possible modality patterns of its extensions. One of these extensions 8f is valid in elliptic planes. These results were presented in his 1980 doctoral dissertation, which is reprinted in this issue of the (...) Australasian Journal of Logic. Here we show that 12g and 8f are strongly complete for validity in their intended one-sorted geometrical interpretations, and have the finite model property. The proofs apply standard technology of modal logic together with a step-by-step procedure introduced by Yde Venema for constructing two-sorted projective planes. (shrink)

Many studies on the astrolabe were written during the period from the ninth to the eleventh century, but very few of them related to projection, i.e., to the geometrical transformation underlying the design of the instrument. Among those that did, the treatise entitled The Art of the Astrolabe, written in the tenth century by Abū Sahl al-Qūhī, represents a particulary important phase in the history of geometry. This work recently appeared in a critical edition with translation and commentary by (...) Roshdi Rashed. It contains the earliest known theory of the projection of the sphere, a theory developed in a commentary written by a contemporary mathematician, Ibn Sahl. Following R. Rashed, the present article offers here a thorough mathematical analysis of al-Qūhī's treatise and of the commentary by Ibn Sahl. It also presents, with commentary, an account of a contemporary treatise on the projection of the sphere, written by al-[Sdotu]āġānī. The latter work is concerned with the conical projection of a sphere on a plane, from a point on an axis of the sphere, other than its pole. The author consciously avoids the case of stereographic projection, but he studies all the other cases of conical projection which, if we employ the terms of al-Qūhī's theory, are compatible with the movement of the instrument. These three texts provide clear evidence of the emergence, during the second half of the tenth century, of a new field of study, that of projective geometry. (shrink)