Formalization of Hilbert's geometry of incidence and parallelism (Q1293015): Difference between revisions

The author first describes how \textit{D. Hilbert} changed the phrasing of his axioms of incidence in the various early editions of his Grundlagen der Geometrie [(Teubner, Leipzig) (1899; JFM 30.0424.01); second edition (1903; JFM 34.0523.01); seventh edition (1930; JFM 56.0481.01)], in which ``bestimmen'' gave way to ``es gibt''. This is seen as a move from ``construction'' to ``existence''. He then finds weaknesses in Hilbert's formalization of geometry, and goes on to present a type-theoretic formalization (with reference to \textit{A. Ranta} [Type-theoretical grammar (Clarendon Press, Oxford) (1994; Zbl 0855.68073)]) of \textit{T. Skolem}'s axiomatics of projective geometry [Norsk Matem. Tidsskr. 1, 1-13 (1919; JFM 47.0011.01)] and of Hilbert's geometry of incidence and parallelism. Reviewer's remarks: The author presents his formalization as one ``by today's standards'', without giving any reason why he deems formalizations in first-order logic (which is what both Hilbert and Skolem had in mind) to be passé.