thesis_access.pdf (605.62 kB)
Download file

A Mechanical Verification of  the Independence of Tarski's  Euclidean Axiom

Download (605.62 kB)
posted on 12.11.2021, 12:57 by Makarios, Timothy James McKenzie

This thesis describes the mechanization of Tarski's axioms of plane geometry in the proof verification program Isabelle. The real Cartesian plane is mechanically verified to be a model of Tarski's axioms, thus verifying the consistency of the axiom system. The Klein–Beltrami model of the hyperbolic plane is also defined in Isabelle; in order to achieve this, the projective plane is defined and several theorems about it are proven. The Klein–Beltrami model is then shown in Isabelle to be a model of all of Tarski's axioms except his Euclidean axiom, thus mechanically verifying the independence of the Euclidean axiom — the primary goal of this project. For some of Tarski's axioms, only an insufficient or an inconvenient published proof was found for the theorem that states that the Klein–Beltrami model satisfies the axiom; in these cases, alternative proofs were devised and mechanically verified. These proofs are described in this thesis — most notably, the proof that the model satisfies the axiom of segment construction, and the proof that it satisfies the five-segments axiom. The proof that the model satisfies the upper 2-dimensional axiom also uses some of the lemmas that were used to prove that the model satisfies the five-segments axiom.


Copyright Date


Date of Award



Te Herenga Waka—Victoria University of Wellington

Rights License

Author Retains Copyright

Degree Discipline


Degree Grantor

Te Herenga Waka—Victoria University of Wellington

Degree Level


Degree Name

Master of Science

Victoria University of Wellington Item Type

Awarded Research Masters Thesis



Victoria University of Wellington School

School of Mathematics, Statistics and Operations Research


Goldblatt, Robert