thesis_access.pdf (605.62 kB)
Download file

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

Download (605.62 kB)
thesis
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.

History

Copyright Date

01/01/2012

Date of Award

01/01/2012

Publisher

Te Herenga Waka—Victoria University of Wellington

Rights License

Author Retains Copyright

Degree Discipline

Mathematics

Degree Grantor

Te Herenga Waka—Victoria University of Wellington

Degree Level

Masters

Degree Name

Master of Science

Victoria University of Wellington Item Type

Awarded Research Masters Thesis

Language

en_NZ

Victoria University of Wellington School

School of Mathematics, Statistics and Operations Research

Advisors

Goldblatt, Robert