Michael Beeson's Research

Utility Link | Utility Link | Utility Link
-->

Tarski Formalization Project: Hard and Easy Theorems

We consider a theorem to be

  • elementary if it has a proof of 15 or fewer steps. Such proofs can usually be found immediately and automatically. (There are a few exceptions, mostly arising from the fact that sometimes what counts as one OTTER step is really a dozen steps by different inference rules.)
  • simple if it has a proof of 16 to 40 steps. Such proofs can often, but not always, be found with the aid of the diagram.
  • hard or difficult if we do not possess a proof of 40 or fewer steps. Several of these theorems could be proved without using the steps of the book proof, by the subformula strategy. There are about 20 of these difficult theorems among the 200 theorems we studied. A succinct list of them is given on our results page.

On this page, we discuss the structure of Szmielew's presentation of Tarski's geometry, and the main theorems of each chapter. This provides background information for understanding the significance of finding formal proofs of these theorems.

We start by emphasizing that all these theorems are derived from Tarski's axioms A1-A10, i.e. without any use of the continuity axiom A11, nor even any use of the related axioms line-circle and circle-circle continuity that Euclid implicitly used. Thus Euclid's construction of an isosceles triangle in Book I, Prop. 1 already uses too much. Moreover, the parallel axiom A10 is not used until Chapter 12, and the upper dimension axiom is allegedly not used, although we used it to repair a gap in Chapter 10. Without circles, it is not at all obvious how to construct isosceles triangles or how to drop or erect perpendiculars. (A perpendicular is dropped from a point not on a line, and erected at a point on a line.) Without these things, it is not clear how to construct the midpoint of an arbitrary segment. These things were all proved for the first time in Gupta's 1965 thesis, written under Tarksi, and these results form the heart of Chapters 7 and 8. The main results of Chapters 5 and 9 also are from Gupta's thesis. In my opinion, Gupta should have been a co-author of the book by Schwäbhauser, Szmielew, and Tarski. The naive reader, remembering Euclid, may fail to realize how difficult it is to prove these things without circles.

We now discuss the chapters of the book one by one. Chapter 1 discusses the axioms; these are also reviewed in our paper. Chapters 2 and 3 contain elementary theorems about congruence and betweenness. The first difficult theorem (a mere 44 steps) is Satz 4.2, the inner five-segment theorem.

In Chapter 5 there is just one difficult theorem, the "connectivity of betweenness": $$ a \neq b \land T(a,b,c) \land T(a,b,d) \rightarrow T(a,c,d) \lor T(a,d,c).$$ This was proved by Gupta in his 1965 thesis. In earlier versions of Tarski's theories, it had been taken as an axiom.

Chapter 6 introduces the relation $sameside(a,p,b)$ , meaning $a$ and $b$ are on the same side of point $p$, i.e. on the same ray emanating from $p$. This is defined as $T(p,a,b) \lor T(p,b,a)$. All the theorems proved about it are elementary. Chapter 6 also introduces the relation of collinearity, $Col(a,b,p)$. There are no hard theorems in Chapter 6.

Chapter 7 defines the reflection $s(a,p)$ of $p$ in $a$. There are three hard theorems in this chapter. The first one is Satz 7.13, that reflection preserves congruence. The second and third ones are both from Gupta's thesis: Satz 7.22 is the Krippenlemma (a technical result needed for the results on perpendicularity in Chapter 8), and Satz 7.25, the culmination of the chapter, is the theorem that the base of an isosceles triangle has a midpoint. That does not yet imply the existence of arbitrary midpoints, since we can't yet construct an isosceles triangle on any given base (without using circles).

Chapter 7 also contains one of Quaife's challenge problems: the diagonals of a quadrilateral with opposite sides equal bisect each other. We have to assume that they do meet, since in 3-space they need not meet and we are not assuming an upper dimension axiom. Quaife was even willing to assume that the meeting point bisects one diagonal. This theorem, according to the criteria given above, is simple, as it has a 22-step proof; but Quaife didn't find that proof in 1990.

Chapter 8 defines right angles and perpendicularity. The main results of this chapter are Gupta's two famous theorems: Satz 8.18 is the "Lotsatz" (existence of dropped perpendiculars), and Satz 8.21 is the existence of erected perpendiculars. The erected perpendicular theorem requires not only a line $L$ as initial data, and a point $a$ on $L$, but also a point $c$ not on $L$, and it constructs not only a point $x$ such that $xa \perp L$, but also a point $t$ on $L$ such that $T(x,t,c)$, so $t$ witnesses that $x$ is on the other side of $L$ from $c$. The construction of the dropped perpendicular uses the theorem that a base of an isosceles triangle has a midpoint, as well as the technical Krippenlemma.

Once we can construct perpendiculars, it is possible to verify Hilbert's midpoint construction. Just erect perpendiculars to segment $ab$ at $a$ and at $b$, on opposite sides of $ab$, lay off an equal distance from $L$ on those two perpendiculars, and connect those two points. That line will meet $ab$ (as has to be shown!) and the point of intersection is the midpoint of $ab$. That is the last theorem, Satz 8.24, in Chapter 8.

Chapter 9 introduces the notions of points $a$ and $b$ being on opposite sides, or on the same side, of a line $L$. They are on the opposite sides if the (open) segment $ab$ meets $L$; they are on the same side if there is a point $c$ such that $a$ and $c$ are on opposite sides of $L$ and $b$ and $c$ are on opposite sides of $L$. (This definition works without an upper dimension axiom, while the definition that $ab$ does not meet $L$ works only in two dimensions.) There are three hard theorems in Chapter 9 about the properties of $samesideline$, including Satz 9.13, that $samesideline$ is a transitive relation between pairs of points. But the main result of Chapter 9 is Gupta's theorem (Satz 9.6) that inner Pasch implies outer Pasch. This belongs in the chapter on sides of lines, because some theorems about sides of lines are used to prove it, and in turn it is used to prove Satz 9.13.

Chapter 10 introduces the notion of the reflection of a point in a line. We use the notation $reflect(a,b,p)$ for the reflection of $p$ in $Line(a,b)$, written as $s_L(p)$ or $s_{ab}(p)$ in the book. The first hard theorem is that reflection in a line preserves congruence.

The next aim of the chapter is to prove Euclid's Postulate 4, that all right angles are equal. This is Satz 10.12. Satz 10.12 is proved in three parts, but in the book those three parts do not get separate names. The first case is this: Two right triangles with congruent legs, a common vertex at the right triangle, and one common leg, have congruent hypotenuses. That part already contains the essence of Euclid's Postulate 4. The general theorem is reduced to that case by two applications of reflection, and the theorem that reflection preserves congruence.

The last part of Chapter 10 derives Hilbert's axiom about triangle construction; given any triangle $abc$, a segment $AB$ congruent to $ab$, and a point $p$ not on $L = Line(A,B)$, we can construct point $C$ on the same side of $L$ as $p$ making triangle $ABC \cong abc$, and moreover $C$ is unique with respect to these requirements.

Chapter 11 develops the theory of angle congruence, treating it as a defined concept, where an angle is given by three points, instead of as a primitive concept (as Hilbert and Euclid both did). This culminates in Satz 11.15, the verification of Hilbert's angle transport axiom. This is the only difficult theorem in Chapter 11.

Chapter 12 uses the parallel axiom for the first time. The main point of the chapter is Satz 12.11, the verification of Hilbert's parallel axiom (thus, Tarki's parallel axiom implies Hilbert's). There is a gap in the proof of Satz 12.11, in that the existence of $c^\prime$ asserted without proof near the beginning of the proof is really rather difficult to prove. We formulated that as a separate lemma and proved Satz 12.11 using that lemma and as well, a case division; so all told, the proof is well over the number of steps required for the label "hard theorem."