Email Gateway (Aug 19 2022 at 09:18): Email Gateway (Aug 19 2022 at 09:18):From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/Tarskis_Geometry.shtml
The independence of Tarski's Euclidean axiom
T. J. M. Makarios
Tarski's axioms of plane geomtry are formalized and, using the standard real
Cartesian model, shown to be consistent. A substantial theory of the projective
plane is developed. Building on this theory, the Klein-Beltrami model of the
hyperbolic plane is defined and shown to satisfy all of Tarski's axioms except
his Euclidean axiom; thus Tarski's Euclidean axiom is shown to be independent of
his other axioms of plane geometry.
An earlier version of this work was the subject of the author's MSc thesis,
which contains natural-language explanations of some of the more interesting proofs.
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC