{{interfaces | imports = Interface:Collinearity | exports = Interface:Connectivity for betweenness }}
This is part of a series of modules which prove a variety of geometrical theorems starting with Tarski's axioms for geometry. We follow the formalization of Julien Narboux<ref>The formal proofs are at http://www.lix.polytechnique.fr/Labo/Julien.Narboux/tarski.html Formalization of Tarski's geometry in the Coq proof assistant and are described in Julien Narboux (2007), "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8614 Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156</ref> which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.<ref>W. Schwabhäuser, W Szmielew, and A. Tarski (1983), ''Metamathematische Methoden in der Geometrie'', ISBN 0387129588</ref>
This page is devoted to the proof of one theorem, A ≠ B ∧ between A B C ∧ between A B D → between A C D ∨ between A D C.<ref>l5_1 in Narboux</ref> This is called outer connectivity for betweenness by Narboux<ref>Narboux (2007), page 144</ref> and Givant.<ref>Tarski and Givant (1999), page 186</ref> It was once considered an axiom of Tarski's system, but was proved from the other axioms by Gupta in 1965<ref>Tarski and Givant (1999), page 190</ref><ref>Narboux (2007), citing Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)</ref>
The proof is not simple; Givant calls it "rather involved" and Narboux devotes two and a half pages to an informal proof (and an explanation of part of the formal proof).<ref>Narboux (2007), pages 151-153</ref>
We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:
thumb|right|construction of C′, D′, B′, and B″
Here's an outline of the proof, illustrating which points we construct but leaving most of the detailed line segment congruences for the detailed formal proof.
We first construct C′ and D′ extending the line segments A D and A C by a distance of C D in both cases. Eventually, the proof will show that C = C′ or D = D′.
Then extend the line segments A C′ and A D′ to points B′ and B″ by distances of C B and D B. The result of this construction is that the distance from B is the same to either B′ or B″ and thus we can conclude that B′ = B″.
{{clear}} thumb|right|construction of E The point E lies at the intersection of C C′ and D D′.
At this point we assume C ≠ C′ and will deduce from that D = D′.
{{clear}} thumb|right|construction of P, Q, and R Extend C′ C by the distance C D′ to a point P. Extend D′ C by the distance C E to a point R. Extend P R by the distance R P to a point Q.
{{clear}} thumb|right|D′ D ≡ P Q and C P ≡ C Q By some congruences we can show first D′ D ≡ P Q, which we'll need at the end of the proof, and C P ≡ C Q, which leads to the next step.
{{clear}} thumb|right|B P ≡ B Q and B′ P ≡ B′ Q thumb|right|C′ P ≡ C′ Q At this point we will apply EquidistantLine five times. In every case we will show that x P ≡ x Q (based on two such existing congruences). For the starting point, we already have C P ≡ C Q and R P ≡ R Q. In turn, we will prove a similar congruence for D′, B, B′, and C′. Those cases easily fit the pictures we have been drawing so far. But we don't stop there: because C′, C, and P are collinear, we can also conclude P P ≡ P Q (this last one doesn't quite as readily lend itself to being illustrated in diagram form, but the first four are illustrated in the adjacent figures).
Of course, P P ≡ P Q implies P = Q, which in turn implies D = D′ (via D D′ ≡ P Q).
We have shown that C ≠ C′ implies D = D′, or in other words C = C′ ∨ D = D′. The former implies A D C and the latter implies A C D, so we reach the conclusion that between A C D ∨ between A D C.
{{clear}} == Construction of C′, D′, B′, and B″ == thumb|right|construction of C′, D′, B′, and B″ We construct c′ such that between A D c′ ∧ D c′ ≡ C D and d′ such that between A C d′ ∧ C d′ ≡ C D.
Then we construct b′ such that between A c′ b′ ∧ c′ b′ ≡ C B and b″ such that between A d′ b″ ∧ d′ b″ ≡ D B.
The following lemma embodies these constructions, and a bit of rearrangement of the quantifiers.
thumb|right|B′ = B″ In this section we'll show that B′ = B″. The idea of the proof is simple: to get from B to B′ we go through D and C′, and to get from B to B″ we go through C and D′. As can be seen from the way we constructed the points, the three segments in the one case are congruent to the three segments in the other (although in reverse order), so the distance from B to either B′ or B″ is the same. Because A ≠ B, this implies that B′ = B″ by the uniqueness of segment construction (applied to A B B′ and A B B″).
thumb|right|B C′ ≡ B″ C Here we prove B C′ ≡ B″ C, starting with a few lemmas which we'll need.
thumb|right|B B′ ≡ B″ B Here we extend the congruence from the previous section one more point. This is also an application of OuterThreeSegment, and we again break out some of the pieces into lemmas.
In this section we apply SegmentConstructionUniqueness to prove that B′ and B″ are in fact the same point. We start with some more betweenness transitivity lemmas.
thumb|right|C′ D′ ≡ C D, construction of E, E C ≡ E C′, and E D ≡ E D′ In this section we construct the point E and also prove a number of congruences. First (even before we construct E), we can apply outer five segment to the line segments B C D′ and B′ C′ D with points C′ and C to give us C′ D′ ≡ C D. Then we construct E as the intersection of C C′ and D D′ (the axiom of Pasch ensures its existence).
The congruences E C ≡ E C′ and E D ≡ E D′ may remind us of the familiar theorem that the diagonals of a rhombus bisect each other, but of course to say it that way would get ahead of ourselves. We can readily prove each of those two congruences, however, from a simple invocation of inner five segment.
thumb|right|C′ D′ ≡ C D We just said that this follows from inner five segment, but that's a slight oversimplification. That's true for the B ≠ C case (which we'll prove first), but there's a separate B = C case. We'll start with the B ≠ C case, and before the case itself we'll prove a few lemmas which represent the various antecedents of OuterFiveSegment.
We now turn to the B = C case. We first note that in this case C′ B′ ≡ C B implies B′ = C′
Finishing the proof of C′ D′ ≡ C D just involves assembling the two cases.
We're now ready to construct the point E. We already have the betweenness relationships we need for the axiom of Pasch, between D′ C A and between C′ D A. Applying Pasch, we get C E C′ and D E D′.
Here's a variant of the previous theorem with the antecedent repeated inside the quantifier.
thumb|right|E C ≡ E C′ and E D ≡ E D′ Here we apply inner five segment to prove E C ≡ E C′. We are applying inner five segment to the line segments D E D′ and D E D′ and points C and C′.
The proof that E D ≡ E D′ is exactly analogous, but applies inner five segment to the line segments C E C′ and C E C′ and points D and D′.
thumb|right|construction of P, Q, and R Extend C′ C by the distance C D′ to a point P. Extend D′ C by the distance C E to a point R. Extend P R by the distance R P to a point Q.
In other words, we are adding (between C′ C P ∧ C P ≡ C D′) ∧ (between D′ C R ∧ C R ≡ C E) ∧ (between P R Q ∧ R Q ≡ R P)
Our goal is to prove C = C′ ∨ D = D′. We do this by adding C ≠ C′ to our antecedent and then showing it implies D = D′. The first step is to show that C ≠ D′. This is a straightforward consequence of C ≠ C′ and the congruence of C D′ and C′ D′, but it will take a few lemmas to do all the needed arranging.
The proof is by outer five segment on D′ C R and P C E and points P and D′. We pretty much have everything we need to apply outer five segment, although between P C E is complicated enough to break out into its own lemma. This lemma follows from between P C C′ and between C E C′.
This is an easy consequence of R P ≡ E D′.
thumb|right|D′ D ≡ P Q and C P ≡ C Q The congruences from the previous section, R P ≡ E D′ and R Q ≡ E D, lead to D′ D ≡ P Q, which is a congruence we'll need later on. The proof is by outer three segment on D′ E D and P R Q.
thumb|right|D′ D ≡ P Q and C P ≡ C Q To prove C Q ≡ C D, there are two cases, based on whether D′ = E or not.
We start with the case in which D′ = E.
First is D′ = D, which follows via E = D from E D ≡ E D′.
It might seem that having proved D′ = D we are done with this case (since after all, D′ = D is the long-term goal of this proof). Although we could, of course, proceed this way, it would entail carrying along the two cases to almost the end of the proof. So we instead will take a few more steps to prove C Q ≡ C D. The next one is P = Q.
Now that we have P = Q, we just need to apply transitivity and a substitution to C P ≡ C D′ and C D′ ≡ C D to get C Q = C D.
The more interesting case is D′ ≠ E. It follows from outer five segment on line segments D′ E D and P R Q and points C and C.
That the previous result implies C P ≡ C Q is apparent from looking at the single ticked line segments in the diagram. The proof is just some congruence transitivity.
thumb|right|D′ P ≡ D′ Q, B P ≡ B Q, and likewise for B′ and C′ We've set up the dominos, and in this section we push them over. For a domino (point) x to "fall" means that we prove x P ≡ x Q (via EquidistantLine). So we need three collinear points, the first two of which are not equal, and the first two of which already have their congruences with P and Q proven. That gives us the third congruence, and then this domino is ready to push on one of the following ones.
We start with R, C, and D′.
The first part is R ≠ C. We will show that R = C implies C = C′, so a transposition gives us what we want.
Now we are ready to prove D′ P ≡ D′ Q.
The next point is B′, which follows from the results for C and D′. We break out one substitution into a lemma, but other than that we have everything we need.
The next point is B, which also follows from the results for C and D′. We have everything we need here with even less work than in the previous section.
The next point is C′, which follows from the results for B and B′.
Before we get to the main proof of this, we prove a few lemmas. The first one we need is between B′ C B. As we already have between B″ C B, this is just a substitution.
The next lemma is B ≠ B′. As usual, this will be via the contrapositive.
The next point is P, which follows from the results for C′ and C. It would be harder to draw a diagram for this one (if the diagram were to show the congruences as well as just P, C, and C′), but the proof is much the same as the ones we've done so far.
Having proved P P ≡ P Q, we are most of the way done.
Here's a variant of CongruenceIdentityFromEquality. Because we (almost?) always want the imported one, the plan is to phase out the exported version in favor of the imported one.
And D = D′ follows from P = Q and P Q ≡ D D′.
In this section we prove that the long list of antecedents we have been working with implies between A C D ∨ between A D C. There are a few steps.
We now are prepared to take the various lemmas which represent the construction of the various points, tie them together (basically just syllogisms, with suitable handling of ∃), and then remove the quantifiers once they are no longer needed.
We now export to Interface:Connectivity for betweenness.
<references/>
{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)