Foundation of geometry in planes, and some complements: Excluding the parallel axioms

Fumiya Iwama

November 22, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

"Foundations of Geometry" is a mathematical book written by Hilbert in 1899. This entry is a complete formalization of "Incidence" (excluding cubic axioms), "Order" and "Congruence" (excluding point sequences) of the axioms constructed in this book. In addition, the theorem of the problem about the part that is treated implicitly and is not clearly stated in it is being carried out in parallel.

License

BSD License

Topics

Session Foundation_of_geometry

Cite

× 
@article{Foundation_of_geometry-AFP,
  author  = {Fumiya Iwama},
  title   = {Foundation of geometry in planes, and some complements: Excluding the parallel axioms},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Foundation_of_geometry.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: