This section will cover basic properties of the congruence predicate, closely following Chapter 2 of Schwabhäuser.
Properties of Congruence
This subsection details properties of congruence with no reference to the betweenness relation.
Our first three theorems justify that if we think about the congruence relation not as a tertiary relation between four points, but as a binary relation between line segments, then congruence is an equivalence relation.
From (A1) we have that ba \equiv ab. Then by (A2) we have
ba \equiv ab \land ba \equiv ab \implies ab \equiv ab.
ab \equiv cd \implies cd \equiv ab
By our hypothesis, ab \equiv cd. Then by congruence reflexivity we have ab \equiv ab. Applying (A2) gives us
ab \equiv cd \land ab \equiv ab \implies cd \equiv ab.
ab \equiv cd \land cd \equiv ef \implies ab \equiv ef
By our hypothesis, ab \equiv cd and cd \equiv ef. By applying congruency transitivity we have cd \equiv ab. Then by (A2) we have
cd \equiv ab \land cd \equiv ef \implies ab \equiv ef.
We can now also show that congruence is commutative on the left and right hand sides, that is
ab \equiv cd \implies ba \equiv cd
By our hypothesis, ab \equiv cd. Then by (A1) we have ab \equiv ba. From (A2) we have
ab \equiv ba \land ab \equiv cd \implies ba \equiv cd.
ab \equiv cd \implies ab \equiv dc
By our hypothesis, ab \equiv cd. Then by (A1) we have cd \equiv dc. From transitivity of congruence we have
ab \equiv cd \land cd \equiv dc \implies ab \equiv dc.
We now move on from permutations of the congruence relation, introducing the congruency of null segments.
Here we use (A4) to assert the existence of x such that
Bbax \land ax \equiv bb.
Then by (A3) we have x = a, and thus aa \equiv bb
The proof above uses a technique that will be applied many times in the development of Elementary Geometry; that is, to show a point a has some property we introduce a point x with said property and prove a = x.
Outer-Five-Segment-Configuration
We now introduce the Outer-Five-Segment-Configuration, denoted \text{OFSC}. (Fünf-Strecken-Konfiguration in Schwabhäuser)
The Outer-Five-Segment-Configuration is an octonary (8-ary) predicate relating two triangles. It is defined
\begin{align*}
\text{OFSC}
\begin{pmatrix}
a & b & c & d\\
a^\prime & b^\prime & c^\prime & d^\prime
\end{pmatrix}
\iff &Babc \land Ba^\prime b^\prime c^\prime \land ab \equiv a^\prime b^\prime \land\\
&bc \equiv b^\prime c^\prime \land ad \equiv a^\prime d^\prime \land bd \equiv b^\prime d^\prime
\end{align*}
[Insert OFSC-Example Diagram]
The use of the definition is that it allows us to rewrite the Five-Segment axiom as
\text{OFSC}
\begin{pmatrix}
a & b & c & d\\
a^\prime & b^\prime & c^\prime & d^\prime
\end{pmatrix} \land a \not = b \implies cd \equiv c^\prime d^\prime.
Thus we can infer the congruence of the ‘Outer’ segments cd and c^\prime d^\prime. In the next chapter, we will introduce the Inner-Five-Segment-Configuration allowing us to infer the congruence of an inner segment.
[Insert Segment-Addition Diagram]
We now turn to the remaining two theorems of this chapter. The first is segment addition, which allows us to ‘add’ two connected segments together.
(Babc \land Ba^\prime b^\prime c^\prime \land ab \equiv a^\prime b^\prime \land bc \equiv b^\prime c^\prime) \implies ac \equiv a^\prime c^\prime
We have from the law of the excluded middle a = b \lor a \not = b, so we break the proof into cases.
Case 1: a \not = b.
We have from our hypothesis
\text{OFSC}
\begin{pmatrix}
a & b & c & a\\
a^\prime & b^\prime & c^\prime & a^\prime.
\end{pmatrix}
Therefore if a \not = b, then by the Five-Segment axiom we have ca \equiv c^\prime a^\prime and thus ac \equiv a^\prime c^\prime by our congruence commutativity theorems.
Case 2: a = b.
If a = b, then we have aa \equiv a^\prime b^\prime. Then by congruence symmetry we have a^\prime b^\prime \equiv aa and (A3) we have a^\prime = b^\prime. Then bc \equiv b^\prime c^\prime \implies ac \equiv a^\prime c^\prime.
Segment addition allows us to show the equivalence of the different forms of the five segment axiom, described previously.
The last theorem of this section is the uniqueness of segment construction, allowing us to prove that two points satisfying the segment construction axiom are the same point. This has the restriction that q \not = a, since otherwise Bqax would be true for all x.
q \not = a \implies \exists! x (Bqax \land ax \equiv bc)
Suppose we have two points x,x^\prime such that Bqax \land ax \equiv bc and Bqax^\prime \land ax^\prime \equiv bc. Then we have ax \equiv ax^\prime by congruence transitivity.
We have Bqax \land Bqax^\prime \land qa \equiv qa \land ax \equiv ax^\prime, thus by segment addition we have qx \equiv qx^\prime. Then we have
\text{OFSC}
\begin{pmatrix}
q & a & x & x\\
q & a & x & x^\prime.
\end{pmatrix}
Thus by (A5) we have xx \equiv xx^\prime. and finally that gives us x = x^\prime by (A3).