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.
Congruence of right triangles; triangle construction and uniqueness
The most important theorem in this chapter is Satz 10.12, which says that two right triangles
with pairwise congruent legs also have congruent hypotenuses.
This is not an immediate consequence of the 5-segment axiom;
the 5-segment axiom together with this theorem implies SAS, but the
5-segment axiom alone does not immediately imply SAS.
Euclid took it as a postulate that all right angles are congruent, which is essentially the
content of Satz 10.12, although angle congruence is not defined until Chapter 11.
Satz 10.12 is proved in three stages:
first we reduce to the case where the two triangles have their right-angled vertex in common
(by reflection in the midpoint of the line joining those vertices). Then we reduce to the case
where they have one leg in common. To that we need a "rotation". Rotation through a given angle
can be done by reflecting in the bisector of that angle. Since we can find the midpoint of a line,
by Gupta's midpoint construction, we can bisect an angle. So, the chapter begins with the definition
and properties of reflection in a line. The only difficult property is that reflection preserves betweenness
(Satz 10.10).
Once Satz 10.12 is in hand, and Gupta's dropped perpendiculars are available, it is an easy
matter to verify Hilbert's axiom about triangle construction and uniqueness (Satz 10.16a and Satz 10.16b).
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 |
| Satz10.2a | Satz10.2a.prf | 45 | hints | | existence of $reflect(a,b,p)$, the reflection of $p$ in $Line(a,b)$ (provided $a\neq b$) | | Satz10.2b | Satz10.2b.prf | 49 | hints | | Uniqueness of the reflection of a point in a line | | Satz10.4 | Satz10.4.prf | 17 | hints | | $reflect(a,b,p) = q$ implies $reflect(a,b,q) = p$ (provided $a \neq =b$). | | Satz10.5 | Satz10.5.prf | 4 | | | $reflect(a,b,reflect(a,b,p)) = p$ (provided $a\neq b$) | | Satz10.6 | Satz10.6.prf | 6 | | | There exists exactly one $x$ such that $reflect(a,b,x) = p$,
namely $x = reflect(a,b,reflect(a,b,p))$. | | Satz10.7 | Satz10.7.prf | 3 | | | Reflection in $Line(a,b)$ is one-to-one:
$reflect(a,b,p) = reflect(a,b,q)$ implies $p=q$. | | Satz10.8a | Satz10.8a.prf | 3 | | | $reflect(a,b,p) = p$ implies $Col(a,b,p)$ (provided $a\neq b$). | | Satz10.8b | Satz10.8b.prf | 3 | | | If $Col(a,b,p)$ then $reflect(a,b,p) = p$ (provided $a\neq b$). | | Satz10.10a | Satz10.10a.prf | 13 | hints | | The case $Col(a,b,p)$ of Satz 10.10. | | Satz10.10 | Satz10.10.prf | 72 | hints | | Reflection preserves congruence:
$ E(p,q,reflect(a,b,p),reflect(a,b,q))$ (provided $a\neq b$).
Our proof uses the lemmas in Satz10.10a.in and Lemma9.3.in. | | Satz10.12b | Satz10.12b.prf | 91 | hints | | Two right triangles with congruent legs, a common vertex at the right triangle,
and one common leg, have congruent hypotenuses. | | Satz10.12c | Satz10.12c.prf | 18 | | | Two right triangles with a common vertex at the right angle and congruent legs have congruent hypotenuses, if two equal legs are collinear on opposite sides of the vertex. This special case is not treated properly in the book. | | Satz10.12a | Satz10.12a.prf | 60 | hints | | Two right triangles with a common vertex at the right angle and congruent legs have congruent hypotenuses, if two equal legs are collinear. | | Satz10.12 | Satz10.12.prf | 26 | hints | | Two right triangles with congruent legs have congruent hypotenuses.
As in the book, we prove this theorem by reducing to 10.12a (common vertex), then to 10.12b (common leg), although in the book these theorems are not given different numbers. | | Satz10.14 | Satz10.14.prf | 10 | diagram | | If $p_1 = reflect(a,b,p)$ and $p$ is not on $Line(a,b)$, then $p$ and $p_1$ are on opposite sides of $Line(a,b)$. | | Satz10.15 | Satz10.15.prf | 74 | hints | | If $b \neq c$ and $Col(b,c,a)$ and not $Col(b,c,q)$, then $bc \perp pa$ and $p$ and $q$ are on the same side of $Line(b,c)$,
where $p = erectsameside(b,c,a,q)$ is constructed in the proof. | | Satz10.16a | Satz10.16a.prf | 44 | hints | | Triangle construction. Given triangle $abc$ and segment $AB$ with $ab=AB$, and point $p$ not on $L = Line(A,B)$, there exists point $C$ on the same side of $L$ as $p$ such that triangle $ABC$ is
congruent to triangle $abc$. | | Satz10.16b | Satz10.16b.prf | 56 | hints | | Triangle uniqueness. Given triangle $abc$ and segment $AB$ with $ab=AB$, and point $p$ not on $L = Line(A,B)$, there do not exist two different
points $C$ on the same side of $L$ as $p$ such that triangle $ABC$ is
congruent to triangle $abc$. |
Back to top of archive
|
