Twoness Show Code edit
thm (Twoness () () (∃ a (∃ b (¬ (= a b))))
a b c TwonessLemma
(∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))))
c (¬ (= a b)) (¬ (= b c)) ThereExistsDisjunctionMovement
(↔ (∃ c (∨ (¬ (= a b)) (¬ (= b c)))) (∨ (¬ (= a b)) (∃ c (¬ (= b c)))))
eliminateBiconditionalReverse
(→ (∃ c (∨ (¬ (= a b)) (¬ (= b c)))) (∨ (¬ (= a b)) (∃ c (¬ (= b c)))))
b addThereExists
(→ (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))) (∃ b (∨ (¬ (= a b)) (∃ c (¬ (= b c))))))
a addThereExists
(→ (∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c)))))) (∃ a (∃ b (∨ (¬ (= a b)) (∃ c (¬ (= b c)))))))
applyModusPonens
(∃ a (∃ b (∨ (¬ (= a b)) (∃ c (¬ (= b c))))))
# We now have <code>∃ a ∃ b (a ≠ b ∨ ∃ c b ≠ c)</code>. We distribute <code>∃ b</code> across the disjunction.
b (¬ (= a b)) (∃ c (¬ (= b c))) ThereExistsDisjunction
(↔ (∃ b (∨ (¬ (= a b)) (∃ c (¬ (= b c))))) (∨ (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c))))))
eliminateBiconditionalReverse
(→ (∃ b (∨ (¬ (= a b)) (∃ c (¬ (= b c))))) (∨ (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c))))))
a addThereExists
(→ (∃ a (∃ b (∨ (¬ (= a b)) (∃ c (¬ (= b c)))))) (∃ a (∨ (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c)))))))
applyModusPonens
(∃ a (∨ (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c))))))
# We have <code>∃ a (∃ b a ≠ b ∨ ∃ b ∃ c b ≠ c)</code>. We move the second disjunct outside of the quantifier for <code>a</code> to get <code>∃ a ∃ b a ≠ b ∨ ∃ b ∃ c b ≠ c</code>
a (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c)))) ThereExistsDisjunctionRightMovement
(↔ (∃ a (∨ (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c)))))) (∨ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c))))))
eliminateBiconditionalReverse
(→ (∃ a (∨ (∃ b (¬ (= a b))) (∃ b (∃ c (¬ (= b c)))))) (∨ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c))))))
applyModusPonens
(∨ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c)))))
# At this point, we can change the variables in the latter disjunct.
a b c TwonessLemma2
(↔ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c)))))
eliminateBiconditionalForward
(→ (∃ b (∃ c (¬ (= b c)))) (∃ a (∃ b (¬ (= a b)))))
(∃ a (∃ b (¬ (= a b)))) disjoinLL
(→ (∨ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c))))) (∨ (∃ a (∃ b (¬ (= a b)))) (∃ a (∃ b (¬ (= a b))))))
applyModusPonens
(∨ (∃ a (∃ b (¬ (= a b)))) (∃ a (∃ b (¬ (= a b)))))
# Having gotten both disjuncts to use the same variables, we are done.
conflateDisjunction
(∃ a (∃ b (¬ (= a b))))
)
edit