Michael Beeson's Research

Utility Link | Utility Link | Utility Link

Tarski Formalization Project Archives


Click on each chapter to see a table of all proofs and input files from that chapter. The posted input files are now all mechanically generated from a master list of theorems. For more information about our methodology see the top page of this project.

These theorems may seem elementary, but because they are all derived without using any continuity axioms (thus no intersecting circles are allowed), some of the proofs are quite difficult. We mention in particular the work of Gupta's 1965 dissertation, which included

  • the transitivity of betweenness (Satz 5.1)
  • the Krippenlemma (Satz 7.22)
  • the fact that the diagonals of a symmetric quadrilateral (opposite sides equal) bisect each other (Satz 7.21)
  • the "Lotsatz" (existence of a perpendicular to a line from a point not on the line, Satz 8.18)
  • the existence of a perpendicular to a line from a point on the line (Satz 8.20)
  • the construction of a midpoint of any segment (Satz 8.22)
  • Chapter 2 Consequences of the congruence axioms A1-A5
    Chapter 3 Simple theorems on betweenness
    Chapter 4 Simple theorems on congruence and betweenness
    Chapter 5 Connectivity of betweenness; inequality of segments
    Chapter 6 Properties of sameside(a,p,b): a and b are on the same side of point p
    Chapter 7 Reflection; Gupta's Krippenlemma;
    the diagonals of a symmetric quadrilateral bisect each other;
    the base of an isosceles triangle has a midpoint.
    Chapter 8 Right angles; existence of perpendiculars; every segment has a midpoint.
    Chapter 8A Extensionality of Perp. These lemmas do not occur in the book.
    Chapter 9 Sides of a line; inner Pasch implies outer Pasch.
    Chapter 9A Some lemmas needed in Chapters 10-12 and the plane separation theorem, whose proof in SST has a gap.
    Chapter 10 Reflections in a line preserve congruence; two right triangles with congruent legs are congruent; copying a triangle on a given segment.
    Chapter 11 Congruence and comparison of angles; SAS, ASA, and ASS congruence theorems. Proofs of Hilbert's axioms about angle congruence.
    Chapter 12 Parallel lines; Satz 12.11 is Hilbert's parallel axiom.