# [isabelle] New AFP entry: The independence of Tarski's Euclidean axiom

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: The independence of Tarski's Euclidean axiom
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Thu, 08 Nov 2012 13:31:45 +0100
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121026 Thunderbird/16.0.2

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!

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*