TwonessLemma
Show Code edit

thm (TwonessLemma () () (∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))))

a b c LowerDimension

(∃ a (∃ b (∃ c (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))))))

# The <code>a = b</code> case involves first picking out <code>¬ between b c a</code>.

(∧

(¬ (between a b c)) (¬ (between b c a)))

(¬ (between c a b))

ConjunctionRightElimination

(→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∧ (¬ (between a b c)) (¬ (between b c a))))

eliminateLeftConjunctInConsequent

(→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (between b c a)))

(= a b) introduceAntecedent

(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (between b c a))))

# Now we prove a substitution, <code>a = b → (¬ between b c a ↔ ¬ between b c b)</code>

b EqualityReflexivity

(= b b)

c EqualityReflexivity

(= c c)

b b c c a b BetweenBuilder

(→ (∧ (∧ (= b b) (= c c)) (= a b)) (↔ (between b c a) (between b c b)))

detach2of3

(→ (∧ (= b b) (= a b)) (↔ (between b c a) (between b c b)))

detach1of2

(→ (= a b) (↔ (between b c a) (between b c b)))

addNegationInConsequent

(→ (= a b) (↔ (¬ (between b c a)) (¬ (between b c b))))

# We combine the substitution with our previous result to get <code>a = b → (¬ between a b c ∧ ¬ between b c a ∧ ¬ between c a b → ¬ between b c b)</code>.

eliminateBiconditionalReverseInConsequent

(→ (= a b) (→ (¬ (between b c a)) (¬ (between b c b))))

applySyllogismInConsequent

(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (between b c b))))

# Now we turn the consequent into <code>b ≠ c</code>,

(↔ (between b c b) (= b c))

addNegation

(↔ (¬ (between b c b)) (¬ (= b c)))

eliminateBiconditionalReverse

(→ (¬ (between b c b)) (¬ (= b c)))

(= a b) introduceAntecedent

(→ (= a b) (→ (¬ (between b c b)) (¬ (= b c))))

applySyllogismInConsequent

(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (¬ (= b c))))

# and add the <code>a ≠ b</code> disjunct.

(¬ (= b c)) (¬ (= a b)) DisjunctionLeftIntroduction

(→ (¬ (= b c)) (∨ (¬ (= a b)) (¬ (= b c))))

(= a b) introduceAntecedent

(→ (= a b) (→ (¬ (= b c)) (∨ (¬ (= a b)) (¬ (= b c)))))

applySyllogismInConsequent

(→ (= a b) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c)))))

# The <code>a ≠ b</code> case is just a matter of arranging formulas for the case elimination and hooking to <code>LowerDimension</code>.

(¬ (= a b)) (¬ (= b c)) DisjunctionRightIntroduction

(→ (¬ (= a b)) (∨ (¬ (= a b)) (¬ (= b c))))

(∨ (¬ (= a b)) (¬ (= b c)))

(∧

(∧

(¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))

) AntecedentIntroduction

(→ (∨ (¬ (= a b)) (¬ (= b c))) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c)))))

applySyllogism

(→ (¬ (= a b)) (→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c)))))

# We combine the cases and finish the proof.

eliminateCases

(→ (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))) (∨ (¬ (= a b)) (¬ (= b c))))

c addThereExists

(→ (∃ c (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b)))) (∃ c (∨ (¬ (= a b)) (¬ (= b c)))))

b addThereExists

(→ (∃ b (∃ c (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b))))) (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))))

a addThereExists

(→ (∃ a (∃ b (∃ c (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b)))))) (∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c)))))))

applyModusPonens

(∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))))

)