formalization of hilbert s geometry of incidence and parallelism
Copyright policy )formalization of hilbert s geometry of incidence and parallelism
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é.
- University of Helsinki Finland
History of mathematics in the 20th century, General theory of linear incidence geometry and projective geometries, History of mathematical logic and foundations, History of geometry, JFM 30.0424.01, JFM 47.0011.01, Hilbert's geometry of incidence and parallelism, type-theoretic formalization, JFM 56.0481.01, Foundations of classical theories (including reverse mathematics), JFM 34.0523.01, formalization of geometry, axiomatics
History of mathematics in the 20th century, General theory of linear incidence geometry and projective geometries, History of mathematical logic and foundations, History of geometry, JFM 30.0424.01, JFM 47.0011.01, Hilbert's geometry of incidence and parallelism, type-theoretic formalization, JFM 56.0481.01, Foundations of classical theories (including reverse mathematics), JFM 34.0523.01, formalization of geometry, axiomatics
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!