Tom Borcherds Undergraduate Dissertation 2016/17

Implementing Tarski's High School Algebra and Tarski's Geometric Axioms in Isabelle/HOL

Supervised by G.Struth

Abstract

Mechanical theorem proving is a valuable part of computer science, providing a complete formalisation of mathematical proofs which otherwise often include small informalities and intuitions that may lead to mistakes. This project utilises a proof assistant known as Isabelle to create complete formalisations of two well-known axiomatic systems, both created by Alfred Tarski. The first of these is Tarski's High School Algebra, designed to posit the question of how well the mathematical rules that students learn in high school describe the natural numbers. A solution has been found to this problem, and the beginnings of that solution are also formalised in this project. THe second axiomatic set is a concise description of elementary geometry, simply named Tarski's Axioms, that have been detailed in 5 different ways since their inception. This project includes a complete formalisation of all 5 axiom sets, as well as a few interesting formalised proofs relating to these axioms.