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. |
