Tarski Formalization Project Archives
Chapter 8: Right angles and perpendiculars
The three main results in this chapter are all due to Gupta (1965): the existence of dropped
and erected perpendiculars, in Satz 8.18 and Satz 8.22, and the application of those results
to the construction of a midpoint of any segment in Satz 8.22.
These proofs by Gupta make no use of any form of the continuity axiom (in particular no circles are involved),
and they also make no use of the parallel axiom, i.e., they use only neutral geometry; and they do not
use the upper dimension axiom either. The proofs rely on Gupta's work in Chapter 7, specifically the fact
that the base of an isosceles triangle has a midpoint and the Krippenlemma.
In these theorems, $R(a,b,c)$ means that $abc$ is a right angle, but the definition allows the "degenerate"
cases in which some of all of the points are collinear or even coincide. By contrast, those cases are not allowed
in the relations $ ab \perp cd $ or $ perpAt(a,b,x,c,d)$, which means that $ab$ and $cd$ are perpendicular at $x$.
$s(a,p)$ is the reflection of $p$ in the point $a$, not to be confused with the reflection of a point in a line,
which cannot be introduced until after the theory of perpendiculars is developed. By $(abc)\cong(def)$ Tarski means
that corresponding sides of the two "triangles" are congruent, even if the points are collinear or equal.
The predicate $M(a,m,b)$ means that $am = mb$; $m$ then turns out to be unique and is called $midpoint(a,b)$.
The book's proof of Satz 8.22 (existence of a midpoint) proceeds by first proving what we call Satz 8.22b (without giving it a separate statment). Then the book says, "by the symmetry of the
hypotheses" we can assume $ap \le qb$. We handle this by making 8.22b a separate theorem, which we then
apply twice to prove 8.22, with different instantiations.
The last theorem in the chapter,
Satz 8.24, is a more detailed statement about the midpoint, which actually gives a term to construct
the midpoint, in terms of the perpendiculars. It is worth noting, however, that since the perpendiculars
might be dropped or erected, SST does not give a single term that always constructs the midpoint. In
addition there is another case distinction in the proof of that theorem, about which of two segments is
the shorter. By "symmetry" it suffices "without loss of generality" to prove just one case, according
to the book, and that is what we do in Satz 8.24a and Satz 8.24b. (Since 8.24 has a conclusion that is
a conjunction, it has to become two files in resolution form.)
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 |
| Satz8.2 | Satz8.2.prf | 5 | | | $R(a,b,c) \rightarrow R(c,b,a)$. | | Satz8.3 | Satz8.3.prf | 13 | | | $R(a,b,c) \land a \neq b \land Col(b,a,d) \rightarrow R(d,b,c)$. | | Satz8.4 | Satz8.4.prf | 3 | | | $R(a,b,c) \rightarrow R(a,b,s(b,c))$ | | Satz8.5 | Satz8.5.prf | 4 | | | $R(a,b,b)$ | | Satz8.6 | Satz8.6.prf | 10 | | | $R(a,b,c) \land T(p,b,c) \land T(a,c,p) \rightarrow b=c$ | | Satz8.7 | Satz8.7.prf | 23 | subformula | 29 | $R(a,b,c) \land R(a,c,b) \rightarrow b=c$ | | Satz8.8 | Satz8.8.prf | 3 | | | $R(a,b,a) \rightarrow a=b$ | | Satz8.9 | Satz8.9.prf | 2 | | | $R(a,b,c) \land Col(a,b,c) \rightarrow a=b \lor c=b$ | | Satz8.10 | Satz8.10.prf | 30 | diagram | | $ R(a,b,c) \land (abc) \cong (pqr) \rightarrow R(pqr)$ | | Satz8.12a | Satz8.12a.prf | 10 | | | $ perpAt(a,b,x,p,q) \rightarrow perpAt(p,q,x,a,b)$ | | Satz8.12b | Satz8.12b.prf | 3 | | | $ab \perp pq \rightarrow pq \perp ab$ | | Satz8.13a | Satz8.13a.prf | 29 | | | Left to right of 8.13 | | Satz8.13b | Satz8.13b.prf | 15 | diagram | | Right to left of 8.13. In a pure first-order treatment this is more difficult than it appears in Szmielew. | | Satz8.14a | Satz8.14a.prf | 11 | diagram | | Perpendicular lines are distinct. | | Satz8.14b | Satz8.14b.prf | 13 | subformula | 332 | if $c$ lies on both $Line(a,b)$ and $Line(p,q)$ and $ab \perp pq$, then $perpAt(a,b,c,p,q)$ | | Satz8.14c | Satz8.14c.prf | 6 | | | Perpendicular lines are perpendicular at only one point. | | Satz8.15 | Satz8.15.prf | 2 | | | $a \neq b \land Col(a,b,x) \land ab \perp cx \rightarrow perpAt(a,b,x,c,x)$ | | Satz8.16a | Satz8.16a.prf | 5 | | | $ a \neq b \land Col(a,b,x) \land Col(a,b,u) \land u \neq x \land ab \perp cx $$ \rightarrow \neg Col(a,b,c) \land R(c,x,u)$ | | Satz8.16b | Satz8.16b.prf | 14 | | | $a\neq b \land Col(a,b,x) \land Col(a,b,u) \land u \neq x \land
\neg Col(a,b,c) \land R(c,x,u) \rightarrow ab \perp cx$ | | Satz8.18a | Satz8.18a.prf | 12 | | | Uniqueness of the perpendicular to a line from a point not on the line. | | Satz8.18 | Satz8.18.prf | 209 | hints | 40 | Lotsatz (dropped perpendicular)
There is a perpendicular to a line from a point not on the line. | | Satz8.20a | Satz8.20a.prf | 30 | hints | | $R(a,b,c) \land M(s(a,c),p,s(b,c)) \rightarrow R(b,a,p)$ | | Satz8.20b | Satz8.20b.prf | 8 | diagram | | $R(a,b,c) \land M(s(a,c),p,s(b,c)) \land b \neq c \rightarrow a \neq p$ | | perp1 | perp1.prf | 16 | diagram | | $ab \perp cd \rightarrow ba \perp cd $ | | Satz8.21a | Satz8.21a.prf | 98 | hints | | (Erected perpendicular)
Given $c$ not on line $L$, and point $a$ on $L$, there is a point $x$ on the opposite side of $L$ from $c$ such that $xa \perp L$. | | Satz8.21 | Satz8.21.prf | 6 | | | Given point $a$ on line $L$, and another point $c$, there is an $x$ such that $xa \perp L$, and a point $t$ on $L$ between $p$ and $c$. This differs from 8.21a only in that $c$ might lie on $L$. | | Satz8.22b | Satz8.22b.prf | 182 | hints | | Given segment $ab$ and perpendiculars $ap$ and $qb$ to $Line(a,b)$, and point $t$ on $Line(a,b)$ between $p$ and $q$,
with $ap \le qb$, then segment $ab$ has a midpoint. | | Satz8.22 | Satz8.22.prf | 22 | hints | | Every segment has a midpoint (Gupta 1965) | | Satz8.24a | Satz8.24a.prf | 177 | hints | 60 | Given segment $ab$ and perpendiculars $ap$ and $qb$, and point $t$ on line $ab$ between $p$ and $q$, with $ap \le qb$ as witnessed by $T(b,r,q)$ and $ap=br$, then segment $ab$ has a midpoint $x$, which
is defined using the Skolem function for inner Pasch. | | Satz8.24b | Satz8.24b.prf | 154 | hints | 60 | Under the hypotheses of 8.24a, the term defining $x$ also gives the midpoint of $pr$. | | Satz8.24 | Satz8.24.prf | 3 | diagram | | Given segment $ab$ and perpendiculars $ap$ and $qb$, and point $t$ on line $ab$ between $p$ and $q$, then segment $ab$ has a midpoint $x$, which is also the midpoint of $pr$.
In other words, we drop the inequality assumption of 8.24a and 8.24b. |
Back to top of archive
|
