Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: The independence of Tarski's Eu...


view this post on Zulip 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: Mar 29 2024 at 01:04 UTC