Michael Beeson's Research

Tarski Formalization Project Archives

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.

Tarski works in $n$ dimensions, i.e., without using an upper dimension axiom (in the chapters we formalized). He defines the concepts "plane" and "coplanar". The plane determined by line $L$ and point $p$ (not on $L$) is the set of points either on $L$, or on the same side of $L$ as $p$, or on the opposite side of $L$ from $p$.

To fix an oversight in Chapter 12 of SST, we needed to prove a version of the plane separation theorem that does not occur in SST; that is Lemma 9.13f described below. We proved that lemma assuming the dimension axiom for $n=2$. One can formulate a similar lemma that should be valid without any dimension axiom, but it looks difficult to prove (having very many cases to deal with, each requiring about six constructed points). Since our aim was to work in two-dimensional geometry, this fix is sufficient. We called this a "lemma" because it doesn't occur in SST, but with a proof length of more than 80 steps, it is really a difficult theorem.

SST does not use the dimension axiom in the first 12 chapters; we use it only in Lemmas 9.13f and 9.13g, which in turn are used only in Lemma 12.11A-3 and hence in Satz 12.11, the verification of Hilbert's parallel axiom.

There are several other lemmas listed below with proof lengths of 7 to 22 steps. These are lemmas that we needed to make other subsequent theorems from SST go through; they became lemmas only when we failed repeatedly to find certain Otter proofs without them. Lemma 9.13b is particularly interesting, since it is one of the few cases where Otter found a really creative, unexpected proof.

The first two lemmas express the extensionality of $samesideline$, i.e. it does not matter which two points are used to specify the line.

The posted input files are now all mechanically generated from a master list of theorems.

The times shown in the following table are not the times required to find the proof, but rather the maximum time allocated to Otter to find the proof. The time is shown only when it had to be longer than the default, which was often 20 seconds when hints were used and 120 seconds when hints were not used.

For more information about our methodology see the top page of this project.

Input File	Proof	Length	Strategy	Seconds	Commentary
ExtSameSide1	ExtSameSide1.prf	16	hints		If $Col(a,b,c)$ and $b,c$ are different from $a$, and $p,q$ are on the same side of $Line(a,b)$, then $p,q$ are on the same side of $Line(a,c)$.
ExtSameSide2	ExtSameSide2.prf	16	hints		If $p,q$ are on the same side of $Line(a,b)$, then $p,q$ are on the same side of $Line(b,a)$.
Lemma9.13a	Lemma9.13a.prf	1			if $p$ and $q$ are on the same side of $Line(a,b)$, then $p$ and $q$ are on the same side of $Line(b,a)$
Lemma9.13b	Lemma9.13b.prf	15			if $u$ and $w $ both lie on $Line(a,b)$ then the midpoint of segment $ uw$ also lies on that line. (Needed in Satz 10.10.)
Lemma9.13c	Lemma9.13c.prf	11		140	if $T(e,d,d1)$ and $p,q$ are on the same side of $Line(e,d1)$, then $p,q$ are on the same side of $Line(e,d)$. SST doesn't need this because lines are sets.
Lemma9.13d	Lemma9.13d.prf	11			if $p,q$ are on the same side of $ Line(a,b)$, then $q,p$ are on the same side of $Line(a,b)$. This is "obvious", but the proof of Lemma 12.11A-2 would not go through without this lemma.
Lemma9.13e	Lemma9.13e.prf	3			A trivial variant of Satz 9.8, but we seem to need it.
Lemma9.13g	Lemma9.13g.prf	22	hints		Assuming the upper dimension axiom A9 for dimension 2, any two perpendiculars to line $L$ at point $p$ are collinear. (Used to prove 9.13f.)
Lemma9.13f-case1	Lemma9.13f-case1.prf	40	hints		Let $e$ be the foot of the perpendicular to $Line(p,q)$ from $r$. Case 1 is when $e=p$.
Lemma9.13f-case2	Lemma9.13f-case2.prf	42	hints		Case 2 is when $e$ and $p$ are not equal.
Lemma9.13f	Lemma9.13f.prf	1			If $r$ and $s$ are not on line $Line(p,q)$, and not on opposite sides of $L$, then they are on the same side of $L$. This relies on the dimension 2 axiom via 9.13g. The proof of length 1 just uses the two cases formulated separately. We could not combine the cases into a single proof.

Back to top of archive