Tarski Formalization Project Archives
Reflection in a point, midpoint of the base of an isosceles triangle, and the Krippenlemma
The reflection of $a$ in $c$ is the unique point $x$ such that $T(a,c,x)$ and $ac = xc$. It is
written $x=s(c,a)$. This chapter presents results from Gupta's thesis that are used in Chapter 8
to help prove his famous results about the existence of perpendiculars. Remember that in this chapter,
we are not using the parallel axiom, any form of continuity (including line-circle and circle-circle continuity),
and not even the upper dimension axiom.
The predicate $M(a,m,b)$ means that $am = mb$; $m$ (if it exists) is unique. Until we prove that it
does exist, we can't introduce the notation $midpoint(a,b)$; but after proving that the base of an isosceles
triangle $abc$, with $ac=bc$, exists, we can introduce $isomidpoint(a,b,c)$ for the midpoint of $ab$.
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 |
| Satz7.2 | Satz7.2.prf | 4 | | | $M(a,m,b) \rightarrow M(b,m,a)$ | | Satz7.3a | Satz7.3a.prf | 2 | | | $M(a,m,b) \rightarrow m=a $ | | Satz7.3b | Satz7.3b.prf | 2 | | | $m=a \rightarrow M(a,m,b)$ | | Satz7.4a | Satz7.4a.prf | 2 | | | $M(p,a,s(a,p))$ | | Satz7.4b | Satz7.4b.prf | 19 | | | Uniqueness of reflection in a point.
$ M(p,a,r) \land M(p,a,q) \rightarrow r=q$ | | Satz7.6 | Satz7.6.prf | 1 | | | $M(p,a,q) \rightarrow q = s(a,p)$ | | Satz7.7 | Satz7.7.prf | 2 | | | $s(a,s(a,p)) = p$ (reflection is an involution).
In the book this is repeated as Satz 7.12. | | Satz7.8 | Satz7.8.prf | 5 | | | $s(a,p)= r \land s(a,q) = r \rightarrow p = q$ | | Satz7.9 | Satz7.9.prf | 1 | | | $s(a,p)= s(a,q) \rightarrow p = q$ | | Satz7.10a | Satz7.10a.prf | 3 | | | $s(a,p)=p \rightarrow p=a$ | | Satz7.10b | Satz7.10b.prf | 4 | | | $ s(a,p) \neq p \rightarrow p \neq a$ | | Satz7.13 | Satz7.13.prf | 99 | subformula | 921 | $ E(p,q,s(a,p),s(a,q))$ | | Satz7.15a | Satz7.15a.prf | 1 | | | Reflection preserves betweenness. | | Satz7.15b | Satz7.15b.prf | 2 | | | Converse of Satz 7.15a | | Satz7.16a | Satz7.16a.prf | 2 | | | Reflection preserves congruence | | Satz7.16b | Satz7.16b.prf | 4 | | | Converse of Satz 7.16a | | Satz7.17 | Satz7.17.prf | 17 | | | Uniqueness of midpoint | | Satz7.18 | Satz7.18.prf | 2 | | | $ s(a,p)=s(b,p)\rightarrow a=b$ | | Satz7.19 | Satz7.19.prf | 7 | subformula | | $ s(a,s(b,p)) = s(b,s(a,p)) \rightarrow a=b $ | | Satz7.20 | Satz7.20.prf | 9 | | | $Col(a,m,b) \land E(m,a,m,b) \rightarrow a=b \lor M(a,m,b)$ | | Satz7.21 | Satz7.21.prf | 26 | hints | | In a quadrilateral with opposite sides equal, the diagonals bisect each other.(It is assumed that the diagonals meet, which is necessary since no dimension axiom is used.) This is one of Quaife's challenge problems. | | Satz7.22a | Satz7.22a.prf | 108 | subformula | 3189 | Gupta's Krippenlemma (an important lemma for Chapter 8),proved with additional assumption $ca_1 \le ca_2$. The
Krippenlemma is derived by two applications of this theorem,
as in the book, but in the book this case is not stated separately. | | Satz7.22b | Satz7.22b.prf | 12 | | | Krippenlemma, stated using abbreviation KF. | | Satz7.22 | Satz7.22.prf | 2 | | | Krippenlemma, stated as in the book (without using the abbreviation KF). | | Satz7.25 | Satz7.25.prf | 114 | hints | | The base of an isosceles triangle has a midpoint. |
Back to top of archive
|
