axnul Show Code edit
# The first thing we do in terms of constructing sets is the empty set.
thm (axnul () () (∃ x (∀ y (¬ (∈ y x))))
# The only set theory axiom we use in the proof is the axiom of separation, which says that given the existence of any set (which is implicit in some of the predicate logic steps), we can construct a subset of it which has no elements. Here is our application of separation, which we will use at the end of the proof (after a bunch of logical steps).
x y z (∧ (∈ y y) (¬ (∈ y y))) SeparationThereExists
(∃ x (∀ y (↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y)))))))
# The proof starts with <code>¬ (y ∈ y ∧ ¬ y ∈ y)</code>
(¬ (∈ y y)) TertiumNonDatur
(∨ (¬ (∈ y y)) (¬ (¬ (∈ y y))))
collectNegationNDN
(¬ (∧ (∈ y y) (¬ (∈ y y))))
# We now add <code>y ∈ z</code> to get <code>¬ (y ∈ z ∧ (y ∈ y ∧ ¬ y ∈ y))</code>
(∈ y z) (∧ (∈ y y) (¬ (∈ y y))) ConjunctionLeftElimination
(→ (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y)))) (∧ (∈ y y) (¬ (∈ y y))))
introduceTransposition
(→ (¬ (∧ (∈ y y) (¬ (∈ y y)))) (¬ (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y))))))
applyModusPonens
(¬ (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y)))))
# We note that <code>y ∈ x ↔ (y ∈ z ∧ (y ∈ y ∧ ¬ y ∈ y))</code> implies itself.
(↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y))))) ImplicationReflexivity
(→ (↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y))))) (↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y))))))
# We detach half the biconditional to get <code>(y ∈ x ↔ (y ∈ z ∧ (y ∈ y ∧ ¬ y ∈ y))) → ¬ y ∈ x</code>
negatedDetachImplicationBiconditionalRight
(→ (↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y))))) (¬ (∈ y x)))
# We're almost there. We just need to add the quantifiers and apply the instance of the axiom of separation that we started with.
y addForAll
(→ (∀ y (↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y)))))) (∀ y (¬ (∈ y x))))
x addThereExists
(→ (∃ x (∀ y (↔ (∈ y x) (∧ (∈ y z) (∧ (∈ y y) (¬ (∈ y y))))))) (∃ x (∀ y (¬ (∈ y x)))))
applyModusPonens
(∃ x (∀ y (¬ (∈ y x))))
)
edit