### Abstract

Tarski's axioms of plane geometry 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.

### License

BSD License

### Topics

- Mathematics/Geometry

### Session Tarskis_Geometry

- Metric
- Miscellany
- Tarski
- Euclid_Tarski
- Linear_Algebra2
- Action
- Projective
- Hyperbolic_Tarski

## Cite

×

Tarskis_Geometry-AFP

    @article{Tarskis_Geometry-AFP,
      author  = {T. J. M. Makarios},
      title   = {The independence of Tarski's Euclidean axiom},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Tarskis_Geometry.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Nov 9, 2012 : Isabelle2012
- Nov 8, 2012 : Isabelle2012