Out lines

From Wikiproofs
Jump to: navigation, search
Used interfaces
Imports
Interface:Line segment inequality
Exports
Interface:Out lines

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[1] which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.[2]

This page gets its name from out lines, that is a predicate (P is-outside A B) which means that P is on the line A B outside the segment A B. We prove a number of results based on that concept, which in turn lead to a number of theorems involving collinearity.

We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:

import (CLASSICAL Interface:Classical_propositional_calculus () ())
import (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())
import (START Interface:Line_segment_inequality (CLASSICAL FIRSTORDER) () Unable to import parameter START(Interface:Line_segment_inequality)[CLASSICAL(Interface:Classical_propositional_calculus)[]+, FIRSTORDER(Interface:First-order_logic_with_quantifiability)[CLASSICAL(Interface:Classical_propositional_calculus)[]+]+]+: Unable to load module Interface:Line_segment_inequality

Out lines defined[edit]

A point P is on the line A B outside the line segment A B if and only if one of those points is between P and the other and P is not equal to either one.[3]

Unknown command

We also state this definition as a theorem.

Unknown command

Relating out lines to existence of a point beyond the outside point[edit]

This section (and the next one) have to do with relating P is-outside A B to a point C for which between A P C and between B P C. The first result says that if between A P C, then between B P C is equivalent to P is-outside A B.[4]

We first tackle the between B P C → P is-outside A B case. This is a straightforward application of BetweennessMiddleConnectivity, which in this case says basically that between A P C and between B P C imply between A B P ∨ between B A P.

Unknown command

The first two parts of the P is-outside A B definition are the inequalities A ≠ P and B ≠ P which we just carry over from the antecedent.

Unknown command

To apply BetweennessMiddleConnectivity, we first need C ≠ P.

Unknown command

Next we need between C P A.

Unknown command

The last thing we will need for BetweennessMiddleConnectivity is between C P B.

Unknown command

Now we apply connectivity to get between P A B ∨ between P B A, which is the only remaining part of the definition of is-outside.

Unknown command

In the other direction, P is-outside A B tells us that either between P A B or between P B A. In the either case, we can apply transitivity with between A P C to get between B P C.

We'll arrange this proof by first rearranging the disjunction and conjunctions, before we worry about transitivity.

Unknown command

First we pick out A ≠ P ∧ between A P C.

Unknown command

Next we take P is-outside A B, unfold the definition, and extract between P A B ∨ between P B A.

Unknown command

Applying distributivity of conjunction over disjunction finishes the job.

Unknown command

Our first transitivity invocation is between B A P ∧ between A P C ∧ A ≠ P → between B P C.

Unknown command

Our second transitivity invocation is between A B P ∧ between A P C → B P C

Unknown command

Now we combine the two.

Unknown command

The existence of a point beyond the outside point[edit]

In this section we show that a point is outside a line segment if and only if there exists a point beyond the outside point. In symbols, P is-outside A B is equivalent to A ≠ P ∧ B ≠ P ∧ ∃ c (C ≠ P ∧ between A P C ∧ between B P C).

We start with the forward implication. Extend A P to a distinct point c (that is, a point for which P ≠ c ∧ between A P c. We can then apply BeyondOut to show that between B P c.[5] Below we present the formal version of this proof, broken down into several lemmas.

Unknown command

At the end of the proof we'll need a copy of P is-outside A B, so we stick it on the proof stack.

Unknown command

Most of the proof of this lemma consists of an application of BeyondOut. The first thing we need is A ≠ P.

Unknown command

Next is B ≠ P

Unknown command

Next is C ≠ P

Unknown command

Last is between A P C.

Unknown command

Applying BeyondOut gives us between B P C ↔ P is-outside A B

Unknown command

Now we detach the P is-outside A B part so we just have between B P C.

Unknown command

The next lemma is just PointConstructionDifferent, together with some rearrangements via commutativity and symmetry.

Unknown command

We now have P is-outside A B → ∀ c (c ≠ P ∧ between A P c → between B P c). Combining this with the previous result gives P is-outside A B → ∃ c (c ≠ P ∧ between A P c ∧ (c ≠ P ∧ between A P c → between B P c)).

Unknown command

To get between B P c is just a matter of modus ponens. The one complication is that we want to keep c ≠ P ∧ between A P c around in addition, so we apply idempotence, associativity, and modus ponens, in that order.

Unknown command

First is P is-outside A B → A ≠ P

Unknown command

Next is P is-outside A B → B ≠ P

Unknown command

Next is the remainder.

Unknown command

We now turn to the reverse direction.[6]

Unknown command

This proof is basically an application of middle connectivity for betweenness, which in this case is c ≠ P ∧ between c P A ∧ between c P B → between P A B ∨ between P B A. First we need c ≠ P

Unknown command

Next is between c P A.

Unknown command

Next is between c P B.

Unknown command

We apply connectivity, remove the quantifier from the consequent, and assemble the result.

Unknown command

Alternate definition in terms of collinearity[edit]

A point is outside a line segment if and only if it is collinear with the endpoints of the segment but not between them. That is, P is-outside A B ↔ collinear A P B ∧ ¬ between A P B.

We first tackle the forward direction.[7] The first lemma is P ≠ A ∧ P ≠ B ∧ between P A B → ¬ between A P B.

Unknown command

First we pick out and rearrange the parts we need, specifically we prove P ≠ A ∧ P ≠ B ∧ between P A B → between P A B ∧ P ≠ A

Unknown command

The geometrical content of this proof is between P A B ∧ between A P B → A = P.

Unknown command

Applying some propositional logic, we rearrange this to between P A B ∧ A ≠ P → ¬ between A P B

Unknown command

Combining this with our first rearrangement, we get the desired result.

Unknown command

The second lemma, A ≠ P ∧ B ≠ P ∧ between P B A → ¬ between A P B, is very similar.

Unknown command

Combining the two previous lemmas we get P is-outside A B → ¬ between A P B.

Unknown command

Collinearity is straightforward.

Unknown command

Combining the last two results gives the forward direction.

Unknown command

Turning our attention to the reverse direction,[8] we have two tasks. The first is to show that P ≠ A and P ≠ B, each of which follows from ¬ between A P B (because either equality holding would make between A P B hold trivially).

Unknown command

Next we show A = P → (between A P B ↔ between P P B), and from it A = P → between A P B.

Unknown command

Proving B = P → between A P B is similar (via B = P → (between A P B ↔ between A P P).

Unknown command

Our other task is to show between P A B ∨ between P B A.

Unknown command

First we show collinear A P B ∧ ¬ between A P B → between P B A ∨ between P A B

Unknown command

That gives us between P B A ∨ between B A P. We just need to rearrange a bit and we are done.

Unknown command

Combining our tasks proves the reverse direction, and combining forward and reverse directions proves the equivalence.

Unknown command

Reflexive, symmetric, and transitive[edit]

Here we present versions of reflexivity, symmetry, and transitivity. You can think of this as dividing a line (excluding the point P itself) into two equivalence classes: those to the left of P and those to the right (we certainly don't have the machinery to say it quite that way, but that is the rough idea).

Reflexivity[edit]

Unknown command

Symmetry[edit]

Unknown command

Transitivity[edit]

Expanding the definitions of the antecedent, we start with

 A ≠ P ∧ B ≠ P ∧ (between P A B ∨ between P B A) ∧
 B ≠ P ∧ C ≠ P ∧ (between P B C ∨ between P C B)

Looking at the betweenness part of that, there are four cases (between P A B ∧ between P B C being the first, between P A B ∧ between P C B, being the second, and so on).

The interesting part is a lemma which handles those four cases; there is also a fair bit of rearranging (in the lemma and in the proof of the actual theorem).

Unknown command

First we break down the four cases.

Unknown command

Now we distribute the B ≠ P into each of the cases.

Unknown command

The first case is B ≠ P ∧ between P A B ∧ between P B C. In all four cases we are showing that the case in question implies between P A C ∨ between P C A. In the current case, between P A C follows from transitivity.

Unknown command

The second case is B ≠ P ∧ between P A B ∧ between P C B. Here we apply inner connectivity for betweenness.

Unknown command

The third case is B ≠ P ∧ between P B A ∧ between P B C. Here we apply outer connectivity for betweenness.

Unknown command

The fourth case is B ≠ P ∧ between P B A ∧ between P C B. In this one between P C A follows from betweenness transitivity.

Unknown command

First we pick out A ≠ P.

Unknown command

Secondly we pick out C ≠ P.

Unknown command

Next we assemble B ≠ P ∧ ((between P A B ∨ between P B A) ∧ (between P B C ∨ between P C B)) and apply our lemma to turn this into between P A C ∨ between P C A.

Unknown command

Line segment construction[edit]

From a given point, in the direction of a second given point, we construct a segment congruent to a given line segment. This is similar to InnerSegmentConstruction but is expressed in terms of is-outside.

Existence[edit]

In this section we prove the existence of such a point. That is, R ≠ A ∧ B ≠ C → ∃ e (A is-outside e R ∧ A e ≡ B C).

The proof consists of applying InnerSegmentConstruction, rearranging, and applying the definition of is-outside. The following lemma expresses most of the rearrangements.[9]

Unknown command

To apply the definition of A is-outside E R, first we need E ≠ A. This follows from B ≠ C and A E ≡ B C, and the first step is picking out those two formulas.

Unknown command

The next step in getting to E ≠ A is to show that B ≠ C ∧ A E ≡ B C → A ≠ E.

Unknown command

Combining that with the previous result and flipping the two sides of the not-equals sign gives us E ≠ A.

Unknown command

Next we need R ≠ A.

Unknown command

Then we need between A E R ∨ between A R E

Unknown command

That's all for A is-outside E R. So the only remaining step is A E ≡ B C

Unknown command

Uniqueness[edit]

The point that we construct this way is also unique. In symbols, R ≠ A ∧ B ≠ C ∧ A is-outside X R ∧ A X ≡ B C ∧ A is-outside Y R ∧ A Y ≡ B C → X = Y.[10]

The proof of uniqueness is more involved than the existence proof. Start by expanding the definitions of is-outside (and removing the redundant copies of R ≠ A) so we now have

 R ≠ A ∧ B ≠ C ∧
 X ≠ A ∧ (between A X R ∨ between A R X) ∧
 A X ≡ B C ∧
 Y ≠ A ∧ (between A Y R ∨ between A R Y) ∧
 A Y ≡ B C

By congruence transitivity, we derive A X ≡ A Y. Then we look at the betweenness relationships. Specifically we want to conclude between A X Y ∨ between A Y X. There are four cases: between A X R ∧ between A Y R → between A X Y ∨ between A Y X by inner connectivity, between A X R ∧ between A R Y → between A X Y by transitivity, between A R X ∧ between A Y R → between A Y X by transitivity, and A ≠ R ∧ between A R X ∧ between A R Y → between A X Y ∨ between A Y X by outer connectivity.

Once we have A X ≡ A Y and between A X Y ∨ between A Y X, X = Y follows from BetweennessOneDistanceUniqueness (applied twice, once to each of the betweenness formulas).

Our first lemma just spells out the four cases.

Unknown command

First is A ≠ R.

Unknown command

Next is between A X R ∨ between A R X

Unknown command

Next is between A Y R ∨ between A R Y

Unknown command

Now we apply distributivity to expand the four cases.

Unknown command

Now we distribute the A ≠ R into each of the cases.

Unknown command

Now we remove A ≠ R from the first three cases, and apply associativity to the fourth.

Unknown command

The first of the four cases is between A X R ∧ between A Y R.

Unknown command

The second case is between A X R ∧ between A R Y.

Unknown command

The third case is between A R X ∧ between A Y R.

Unknown command

The fourth case is A ≠ R ∧ between A R X ∧ between A R Y.

Unknown command

We first arrange the results of the two previous lemmas to get (between A X Y ∧ A X ≡ A Y) ∨ (between A Y X ∧ A X ≡ A Y).

Unknown command

The result for the first half is between A X Y ∧ A X ≡ A Y → X = Y, which follows directly from BetweennessOneDistanceUniqueness.

Unknown command

The second half result, between A Y X ∧ A X ≡ A Y → X = Y, is basically the same thing, but we need to rearrange slightly.

Unknown command

Now we combine the two halves.

Unknown command

The closer point is between[edit]

If A and B are on a line with P, both on the same side of P, and A is closer to P than B is, then A is between P and B. That is, P is-outside A B ∧ P A ≤ P B → between P A B.[11]

The proof begins by expanding P A ≤ P B to ∃ y (between P y B ∧ P A ≡ P y). From P is-outside A B and P A ≡ P y we can conclude P ≠ y. We will then be applying OutSegmentConstructionUniqueness which in this case expands to:

 B ≠ P ∧ P ≠ y ∧
 P is-outside y B ∧ P y ≡ P y ∧
 P is-outside A B ∧ P A ≡ P y →
 y = A

Each piece of this is something we already have, or readily follows from things we have. Once we have y = A we just substitute it into between P y B and we are done.

The first lemma constructs the point y.

Unknown command

The next lemma is P ≠ y

Unknown command

First we pick out P ≠ A.

Unknown command

Next is P A ≡ P Y.

Unknown command

Next is P = Y ∧ P A ≡ P Y → P = A (from CongruenceIdentityFromEquality), which we then rearrange to give P ≠ A ∧ P A ≡ P Y → P ≠ Y

Unknown command

Combining that with the previous result finishes the proof.

Unknown command

The next lemma is P is-outside Y B.

Unknown command

First we need Y ≠ P.

Unknown command

Then we need B ≠ P.

Unknown command

Finally we need between P Y B ∨ between P B Y.

Unknown command

The next lemma applies OutSegmentConstructionUniqueness to give Y = A.

Unknown command

First we need B ≠ P.

Unknown command

Next we need P ≠ Y.

Unknown command

Next we need P is-outside Y B.

Unknown command

Next is P Y ≡ P Y.

Unknown command

Next is P is-outside A B.

Unknown command

Next is P A ≡ P Y.

Unknown command

Now that we have all the hypotheses, we'll apply OutSegmentConstructionUniqueness to give Y = A.

Unknown command

Now that we have Y = A, we just substitute that into between P Y B to get between P A B.

Unknown command

First we get out Y = A and between P Y B.

Unknown command

The substitution is Y = A → (between P Y B ↔ between P A B).

Unknown command

The point which is between is closer[edit]

The converse also holds: P is-outside A B ∧ between P A B → P A ≤ P B.[12] To prove P A ≤ P B, we need ∃ c (between P c B ∧ P A ≡ P c), and the point A suffices for the choice of c. In fact, we don't need the hypothesis P is-outside A B, so unlike Narboux we state the theorem without it.

Unknown command

Now we apply a substitution c = A → (between P c B ∧ P A ≡ P c ↔ between P A B ∧ P A ≡ P A) to turn between P A B ∧ P A ≡ P A into [ A / c ] (between P c B ∧ P A ≡ P c).

Unknown command

Turning the substitution into ∃ and applying LessEqualCutoff we are done.

Unknown command

Biconditional[edit]

Here we combine the previous two results: P is-outside A B → (P A ≤ P B ↔ between P A B).

Unknown command

Collinearity[edit]

In this section we prove a number of results involving collinearity.

Outer transitivity[edit]

Here we prove P ≠ Q ∧ collinear P Q A ∧ collinear P Q B → collinear P A B.[13] We call it "outer" transitivity although unlike similar-looking results for betweenness, five segment, etc, this does not make it a different theorem than inner transitivity, just a different rearrangement (since the order of points in a collinearity predicate does not matter).

Actually, we first prove it in the slightly rearranged form P ≠ Q ∧ collinear S P Q ∧ collinear X P Q → collinear X P S (in which P and Q are interchanged and the order of the points in the collinearity statements are changed). There is no deep reason for this rearrangement, but it will be slightly more convenient in the next section.

Expanding each collinear in the antecedent by the definition, and then applying associativity, gives us nine cases. In each case we'll be able to prove between X P S, between P X S, between P S X, or a disjunction between two of them. Each case will follow from either betweenness transitivity or betweenness connectivity.

We start with a lemma, and then proceed to the proof.

Unknown command

We prove collinear X P S via its definition: between X P S ∨ between P S X ∨ between S X P.

Unknown command

First we associate the two collinearity formulas together.

Unknown command

Now we apply distributivity multiple times to separate out the nine cases. Round one: splitting collinear S P Q halfway.

Unknown command

Round two: splitting collinear S P Q the rest of the way.

Unknown command

Round three: split collinear X P Q halfway.

Unknown command

Round four: split collinear X P Q the rest of the way.

Unknown command

Having split out the nine cases, we combine with P ≠ Q and then distribute P ≠ Q into each of the cases.

Unknown command

Round one.

Unknown command

Round two.

Unknown command

Round three.

Unknown command

Round four.

Unknown command

Sorry breaking out the cases took so long. Anyway, we are ready to tackle them one by one. The first is between S P Q ∧ between X P Q (of course, all of them have P ≠ Q tacked on the front, which we usually will not state explicitly). It follows from the following application of BetweennessMiddleConnectivity: Q ≠ P ∧ between Q P S ∧ between Q P X → between P S X ∨ between P X S

Unknown command

To finish the first case we turn between P S X ∨ between P X S into collinear X P S.

Unknown command

The second case is between S P Q ∧ between P Q X. This follows from between S P Q ∧ between P Q X ∧ P ≠ Q → between S P X, which is an instance of BetweennessOuterTransitivity.

Unknown command

Now we need between S P X → collinear X P S.

Unknown command

The third case is between S P Q ∧ between Q X P, which follows from between S P Q ∧ between P X Q → between S P X, which is an instance of BetweennessInnerTransitivity

Unknown command

To finish this case we need between S P X → collinear X P S.

Unknown command

We now start the second set of cases, those starting with between P Q S. The fourth case is between P Q S ∧ between X P Q, which follows from between X P Q ∧ between P Q S ∧ P ≠ Q → between X P S, which is an instance of BetweennessOuterTransitivity.

Unknown command

To finish this case we need between X P S → collinear X P S.

Unknown command

The fifth case is between P Q S ∧ between P Q X. This follows from BetweennessOuterConnectivity, which in this case is P ≠ Q ∧ between P Q S ∧ between P Q X → between P S X ∨ between P X S.

Unknown command

To finish this case we turn between P S X ∨ between P X S into collinear X P S.

Unknown command

The sixth case is between P Q S ∧ between Q X P. It follows from between P X Q ∧ between P Q S → between P X S, an instance of BetweennessMiddleTransitivityFlipped

Unknown command

To finish the case we turn between P X S into collinear X P S.

Unknown command

We are ready for the last trio of cases, those which start with between Q S P. The seventh case is between Q S P ∧ between X P Q. It follows from between X P Q ∧ between P S Q → between X P S, which is an instance of BetweennessInnerTransitivity.

Unknown command

To finish the case we turn between X P S into collinear X P S.

Unknown command

The eighth case is between Q S P ∧ between P Q X. It follows by between P S Q ∧ between P Q X → between P S X which is an instance of BetweennessMiddleTransitivityFlipped.

Unknown command

To finish the case we need to turn between P S X into collinear X P S.

Unknown command

The ninth and final case is between Q S P ∧ between Q X P. It follows from between P S Q ∧ between P X Q → between P S X ∨ between P X S, which is an instance of BetweennessInnerConnectivity.

Unknown command

To finish this case, we turn between P S X ∨ between P X S into collinear X P S.

Unknown command

To finish the proof, we simply combine the breaking down of the cases with the resolution of each case.

Unknown command

Now we return to P ≠ Q ∧ collinear P Q A ∧ collinear P Q B → collinear P A B.

Unknown command

First we need P ≠ Q

Unknown command

Second we need collinear A P Q.

Unknown command

Lastly we need collinear B P Q.

Unknown command

Applying the previous rearrangement of transitivity gives us collinear B P A, which we then rearrange to collinear P A B.

Unknown command

Being collinear to collinear points[edit]

Given three collinear distinct points, a fourth point being collinear to two of them is equivalent to being collinear to two others. More precisely, P ≠ Q ∧ S ≠ P ∧ collinear S P Q → (collinear X P Q ↔ collinear X P S).

The forward direction is P ≠ Q ∧ S ≠ P ∧ collinear S P Q ∧ collinear X P Q → collinear X P S.[14] It is almost identical to what we proved in the previous section (we just need to drop the S ≠ P).

Unknown command

The reverse direction is P ≠ Q ∧ S ≠ P ∧ collinear S P Q ∧ collinear X P S → collinear X P Q.[15] This is essentially the same as the forward direction, as exchanging S and Q doesn't really change the statement. Narboux proves the reverse direction by copy-pasting the proof of the forward direction, interchanging S and Q, but our proof simply performs the right rearrangements to apply the forward direction.

Unknown command

We first need P ≠ S.

Unknown command

Next is Q ≠ P.

Unknown command

Next is collinear Q P S.

Unknown command

Last is collinear X P S.

Unknown command

Applying the forward theorem, with S and Q interchanged, finishes the job.

Unknown command

We combine the two previous results to get P ≠ Q ∧ S ≠ P ∧ collinear S P Q → (collinear X P Q ↔ collinear X P S)

Unknown command

Inner transitivity[edit]

Here we prove P ≠ Q ∧ collinear P Q A ∧ collinear P Q B → collinear Q A B.[16] As we said before, the mathematical meaning of the theorem is not different from the "outer" collinearity transitivity; it is merely a rearrangement.

Unknown command

We will be applying collinearity outer transitivity. First we need Q ≠ P.

Unknown command

Next is collinear Q P A.

Unknown command

Last is collinear Q P B.

Unknown command

The intersection of two lines[edit]

If two distinct, non-degenerate lines intersect, they intersect in a single point. At least for this theorem, we consider a line A B and line C D to be distinct and non-degenerate if ¬ collinear A B C ∧ C ≠ D. The statement of the whole theorem is ¬ collinear A B C ∧ C ≠ D ∧ collinear A B P ∧ collinear A B Q ∧ collinear C D P ∧ collinear C D Q → P = Q.[17]

The proof consists of multiple applications of collinearity transitivity, together with some cases and a proof by contradiction. It starts with collinear C P Q (by collinearity transitivity).

Unknown command

C ≠ D:

Unknown command

collinear C D P:

Unknown command

collinear C D Q:

Unknown command

Then note that A ≠ B (as a consequence of ¬ collinear A B C), and collinearity transitivity gives us collinear A P Q and collinear B P Q.

Unknown command

We pick out ¬ collinear A B C, which we will need shortly.

Unknown command

The next step is to note collinear A A C and apply a substitution to turn it into A = B → collinear A B C.

Unknown command

Now we just transpose and combine with ¬ collinear A B C.

Unknown command

A ≠ B:

Unknown command

collinear A B P:

Unknown command

collinear A B Q:

Unknown command

We now assume P ≠ Q and will show collinear A B C, which is a contradiction. The first thing we get from P ≠ Q is collinear A C Q (from collinear A P Q and collinear C P Q).

Unknown command

P ≠ Q:

Unknown command

collinear P Q A:

Unknown command

collinear P Q C:

Unknown command

Transitivity produces collinear Q A C, which we then rearrange to collinear A C Q.

Unknown command

In a similar way we prove collinear A B Q.

Unknown command

P ≠ Q:

Unknown command

collinear P Q A:

Unknown command

collinear P Q B:

Unknown command

Transitivity produces collinear Q A B, which we then rearrange to collinear A B Q.

Unknown command

Now we consider two cases: Q = A and Q ≠ A.

For the Q = A case, first apply collinearity transitivity to collinear C P Q and collinear B P Q to get collinear C B Q, which turns into our desired contradiction collinear A B C by substituting A for Q.

Unknown command

P ≠ Q:

Unknown command

collinear P Q B:

Unknown command

collinear P Q C:

Unknown command

Applying transitivity yields collinear Q B C, which we then turn into collinear A B C via a subsitution.

Unknown command

The Q ≠ A case lets us apply transitivity to collinear A C Q and collinear A B Q to get collinear A B C, which is our desired contradiction.

Unknown command

Q ≠ A:

Unknown command

collinear Q A B:

Unknown command

collinear Q A C:

Unknown command

Next we combine the cases.

Unknown command

Here we point out the contradiction.

Unknown command

Since assuming P ≠ Q produced a contradiction, we can conclude that P = Q.

Unknown command

The existence of a point not on a given line[edit]

Given a line, there is a point which is not on that line. Formally, A ≠ B → ∃ c ¬ collinear A B c.[18]

The proof, not surprisingly, is based on LowerDimension, which gives us three non-collinear points x, y, and z. If any one of them is not on the line (that is, ¬ collinear A B x or likewise for y or z), we are done. But if they are all collinear with A and B, we can conclude collinear x y z by transitivity, which is a contradiction.

We start by restating LowerDimension in terms of collinearity.

Unknown command

The next lemma says that if we have a point not collinear with A and B, we are done.

Unknown command

We're ready to start working on getting collinear x y z by transitivity. There are two cases: A = X and A ≠ X. The A = X case is the easier one: we first conclude collinear A Y Z and then substitute X for A.

Unknown command

A ≠ B:

Unknown command

collinear A B Y:

Unknown command

collinear A B Z:

Unknown command

Applying transitivity gives collinear A Y Z,

Unknown command

and applying a substitution turns that into collinear X Y Z.

Unknown command

The A ≠ X case involves first proving collinear A X Y and collinear A X Z (each by transitivity), and applying transitivity again, to get collinear X Y Z.

Unknown command

We start with A ≠ X.

Unknown command

To prove collinear A X Y, we first need A ≠ B:

Unknown command

collinear A B X:

Unknown command

collinear A B Y:

Unknown command

That's all we need for collinear A X Y

Unknown command

Now we need collinear A X Z, and the first antecedent is A ≠ B.

Unknown command

collinear A B X:

Unknown command

collinear A B Z:

Unknown command

Applying transitivity we get collinear A X Z

Unknown command

We are now ready to apply transitivity to A ≠ X, collinear A X Y, and collinear A X Z to get collinear X Y Z.

Unknown command

We now combine the A = X and A ≠ X cases and rearrange a bit.

Unknown command

The next lemma gets rid of collinear A B X (because the case ¬ collinear A B X is taken care of by PointNotOnLineLemma).

Unknown command

First, the collinear A B X case:

Unknown command

Second, the ¬ collinear A B X case:

Unknown command

Now we just need to combine the cases.

Unknown command

In a very similar manner we get rid of collinear A B Y.

Unknown command

First, the collinear A B Y case:

Unknown command

Second, the ¬ collinear A B Y case:

Unknown command

Now we just need to combine the cases.

Unknown command

At this point we are very close. The only thing remaining in the antecedent that we need to get rid of is ¬ collinear X Y Z. But X, Y, and Z no longer appear anywhere else in the formula. So we can quantify at will, specifically to turn ¬ collinear X Y Z into ∃ x ∃ y ∃ z ¬ collinear x y z, which we can then detach as it is a theorem.

Unknown command

First we put the theorem on the proof stack.

Unknown command

Now we show we can move the quantifiers to the start: A ≠ B ∧ ∃ x ∃ y ∃ z ¬ collinear x y z → ∃ x ∃ y ∃ z (A ≠ B ∧ ¬ collinear x y z)

Unknown command

Now we can introduce the previous theorem and then add the quantifiers.

Unknown command

Detaching the theorem finishes the proof.

Unknown command

Intersecting lines and congruences[edit]

Theorem t2 8 from Narboux.svg

Given two intersecting line segments, where the portions of each segment on the sides of the intersection are congruent, the segments drawn from the endpoints of one line segment to the endpoints of the other are congruent. That is, between A B C ∧ between D B E ∧ A B ≡ D B ∧ B C ≡ B E → A E ≡ C D.[19]

We consider A = B and A ≠ B cases. The A = B case is easy: A = B implies D = B and substituting into B C ≡ B E gives us A E ≡ C D.

The A ≠ B case follows from outer five segment, using baselines A B C and D B E and points D and A.

Starting on the A = B case, the first step is proving D = B.

Unknown command

To apply CongruenceIdentityFromEquality, we first need A = B.

Unknown command

Secondly, we need A B ≡ D B.

Unknown command

That lets us conclude D = B.

Unknown command

We'll need B C ≡ B E a bit later, so we put it on the proof stack.

Unknown command

The next step is the substitution. The substitution will be D = B ∧ A = B → (D C ≡ A E ↔ B C ≡ B E), so we start with D = B ∧ A = B.

Unknown command

Here is D = B ∧ A = B → (D C ≡ A E ↔ B C ≡ B E), as promised.

Unknown command

Pulling B C ≡ B E off the proof stack and combining, we get D C ≡ A E.

Unknown command

Now we just rearrange that congruence to A E ≡ C D.

Unknown command

Now we are ready for the A ≠ B case, in which we apply outer five segment using baselines A B C and D B E and points D and A.

Unknown command

First we need A ≠ B.

Unknown command

We need two betweenness relationships, the first of which is between A B C.

Unknown command

The other is between D B E.

Unknown command

There are two congruences for the baseline, A B ≡ D B,

Unknown command

and B C ≡ B E.

Unknown command

The off-baseline congruences are A D ≡ D A,

Unknown command

and B D ≡ B A.

Unknown command

Applying five segment gives us C D ≡ E A, which we then rearrange to A E ≡ C D.

Unknown command

Export[edit]

We now export to Interface:Out lines.

Unknown command

References[edit]

  1. The formal proofs are at Formalization of Tarski's geometry in the Coq proof assistant and are described in Julien Narboux (2007), "Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156
  2. W. Schwabhäuser, W Szmielew, and A. Tarski (1983), Metamathematische Methoden in der Geometrie, ISBN 0387129588
  3. Definition out in Narboux
  4. l6_2 in Narboux
  5. l6_3_1 in Narboux
  6. l6_3_2 in Narboux
  7. l6_4_1 in Narboux
  8. l6_4_2 in Narboux
  9. l6_11_existence in Narboux
  10. l6_11_unicity in Narboux
  11. l6_13_1 in Narboux
  12. l6_13_2 in Narboux
  13. col_transitivity_1 in Narboux
  14. l6_16_1 in Narboux
  15. l6_16_2 in Narboux
  16. col_transitivity_2 in Narboux
  17. l6_21 in Narboux
  18. l6_25 in Narboux
  19. Theorem t2_8 in Narboux
  • Tarski, Alfred; Givant, Steven (1999), "Tarski's system of geometry", The Bulletin of Symbolic Logic 5 (2): 175–214, doi:10.2307/421089, MR1791303, ISSN 1079-8986