The axioms of constructive geometry (Q1902978): Difference between revisions

The author axiomatizes in \textit{P. Martin-Löf}'s constructive type theory [Logic, methodology and philosophy of science VI, Hannover 1979, Stud. Logic Found. Math. 104, 153-175 (1982; Zbl 0541.03034)] four constructive geometric theories (apartness, projective, affine, and orthogonal geometry). There are two types of individual variables, ``points'' and ``lines'', and as primitive notions the predicates \textit{DiPt}, \textit{DiLn}, \textit{Con}, \textit{Apt}, and \textit{Unort} (used only in the case of orthogonal geometry), whose intended interpretations are: \textit{DiPt}\((a,b)\): ``\(a\) and \(b\) are distinct points'', \textit{DiLn}\((l,m)\): ``\(l\) and \(m\) are distinct lines'', \textit{Con}\((l,m)\): ``\(l\) and \(m\) are convergent lines'', \textit{Apt}\((a,l)\): ``point \(a\) is apart from line \(l\)'', \textit{Unort}\((l,m)\): ``the lines \(l\) and \(m\) are not orthogonal''. Besides general rules of logical (intuitionistic type-theoretical) inference, the axiomatizations consist of rules of construction (allowing the construction of: (i) the line joining two distinct points; (ii) the point that convergent lines have in common, (iii) the line parallel to a given line passing through a given point (for affine and orthogonal geometry), (iv) the line orthogonal to a given line passing through a given point (for orthogonal geometry) and a list of universal axioms. About half of the paper is devoted to the presentation of the axioms and rules of construction and to proofs of very basic results inside the proposed axiom systems. The other half is concerned with the solution of basic geometric constructions (called ``problems'' in the text), a re- axiomatization of the four geometries in higher-level type theory, with computer implementation in the ALF (``Another Logical Framework'') system, where the solving of geometric problems can be done as proof-editing. Previous intuitionistic axiomatizations of (affine and projective) geometry (\textit{A. Heyting} [Math. Ann. 98, 491-538 (1927; JFM 53.0541.01); Stud. Logic Found. Math, Axiomatic Method, 160-173 (1959; Zbl 0092.25002)], \textit{D. van Dalen} [Indag. Math. 25, 349-368, 369-383 (1963; Zbl 0127.11304 and Zbl 0132.40602)]) have addressed the problem of algebraization (coordinatization) of the axiomatically presented geometries (as most axiomatics since Hilbert do), as well as the problem of extending an affine plane to a projective closure. By contrast, the geometries introduced in this paper are so weak that coordinatization is, with the exception of projective geometry, impossible. Whereas apartness geometry is weak by design, for it is intended to be the common part of the other three geometries, there is no apparent reason why affine and orthogonal geometry are provided with rudimentary, underdetermined axiom systems. There is a lot of genuinely geometric work that needs to be done to round out these investigations.