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


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.


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