Betweenness Properties
This section will cover Chapter 3 of SST, which proves many facts about the betweenness relation.
Theorems
We begin with some betweenness identity theorems.
Babb
From segment construction (A4) we have that
\exists c (Babc \land bc \equiv xy).
Choosing x,y to both be b gives us
\exists c (Babc \land bc \equiv bb).
By (A3) we have bc \equiv bb \implies c = b. Thus we have
Babb.
Since our choice of a,b were arbitrary, this holds for all points a,b.
Baaa
Simply apply our previous betweenness identity with a=b, yielding Baaa for all a.
Baab
From Pasch’s axiom (A7) we have that
(Bapc \land Bbqc) \implies \exists x (Bpxb \land Bqxa).
Since we have Bbbb and Bbaa from our previous betweenness axioms, we have
(Baaa \land Bbaa) \implies \exists x (Baxb \land Baxa).
By (A6) we have that Baxa \implies x = a. Thus for all a,b we have
Baab.
Next we have our symmetry theorem.
Babc \implies Bcba
From Pasch’s axiom (A7) we have
(Babc \land Bbcc) \implies \exists x (Bbxb \land Bcxa).
And from (A6) we have Bbxb \implies x = b. We always have Bbcc by our first betweenness identity, so we have
Babc \implies Bbbb \land Bcba
and by conjunction elimination we have
Babc \implies Bcba.
Babc \land Bbac \implies a = b
From Pasch’s axiom (A7) we have
Babc \land Bbac \implies \exists x (Bbxb \land Baxa).
From (A6) we have Bbxb \implies x = b and Baxa \implies x = a. Since x = a and x = b, we have a = b. Thus
Babc \land Bbac \implies a = b.