This section will cover Chapter 2 of SST, which proves many facts about the congruence relation.
Theorems
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 continue to Theorem 2.8. The gap in the theorem numbers is due to SST’s including definitions and remarks in the same numbering sequence as theorems.
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
(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 logic that a = b \lor a \not = b. If a \not = b, then the proof is simply (A5). 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.
q \not = a \implies \exists! x (Bqax \land ax = bc)