# Is it possible to prove empty set uniqueness in FOL directly (without proof by contradiction)

So I have a partial proof of uniqueness of the empty set in FOL:

1. $$\exists x \forall z(z \notin x)$$ (ZF2)
2. $$z_1 \notin e_1$$ (Universal & Existential Instantiation of (1))
3. $$z_1 \notin e_2$$ (Same)
4. $$z_1 \in e_1 \rightarrow z_1 \in e_2$$ (Tautology $$\neg A \rightarrow (A \rightarrow B)$$)
5. $$z_1 \in e_2 \rightarrow z_1 \in e_1$$ (Same)
6. $$\forall z (z \in e_1 \rightarrow z \in e_2)$$ (Uni Generalization)
7. $$\forall z (z \in e_2 \rightarrow z \in e_1)$$ (Same)
8. $$\forall z (z \in e_1 \rightarrow z \in e_2) \land \forall z (z \in e_2 \rightarrow z \in e_1)$$ (Conj Intro)
9. $$\forall z (z \in e_1 \rightarrow z \in e_2 \land z \in e_2 \rightarrow z \in e_1)$$ (Identity)
10. $$\forall z (z \in e_1 \leftrightarrow z \in e_2)$$ (Biconditional Intro)
11. $$e_1 = e_2$$ (Eq Intro)

So far, so good. But what I actually want to prove is: $$\forall x \forall y [(\forall z (z \notin x) \land \forall z (z \notin y)) \rightarrow x = y] .....P$$

As hard as I try, I can't go from (1)-(11) to $$P$$.

Basically where I'm struggling is turning the $$e$$'s into $$\forall$$ statements. Since $$e$$'s are constants, we can only do existential generalization, not universal generalization. I guess my question boils down to whether there is some theorem that allows us to go from constants/existential quantifiers to universal ones. My suspect is "$$(\exists x P(x))\rightarrow Q$$ is equivalent to $$\forall x (P \rightarrow Q)$$ (as long as $$x$$ is not in $$Q$$)", but I can't seem to put the pieces together in the right way. ;)

Everyone seems to agree that it is possible to prove empty set uniqueness directly (e.g. [1]), but I can't find a proof myself...

• The uniqueness of the empty set needs Extensionality. Jan 25 '20 at 12:11
• The empty set is an object that "lives" in set theory; thus you needs the axioms of set theory to manage it. Jan 25 '20 at 12:12
• Yes, I believe I'm using that in Step 11. I should have said I am also using axioms of Set theory. Jan 25 '20 at 12:13
• The question is still the same: is it possible to deduce the theorem directly, only using FOL + set theory axioms? Jan 25 '20 at 12:13
• Yes: using Extensionality, Jan 25 '20 at 13:41

I think I got it!

I'm going to write a bunch of implications and then join the first and last:

$$\quad \forall z (z \notin x) \land \forall z (z \notin y)$$

$$\rightarrow \forall z (z \notin x), \forall z (z \notin y)$$ (Conj Elim)

$$\rightarrow z \notin x, z \notin y$$ (Univ Inst)

$$\rightarrow z \in x \rightarrow z \in y, z \in y \rightarrow z \in x$$ (Tautology $$\neg A \rightarrow (A \rightarrow B))$$

$$\rightarrow z \in x \rightarrow z \in y \land z \in y \rightarrow z \in x$$ (Conj Intro)

$$\rightarrow \forall z (z \in x \rightarrow z \in y \land z \in y \rightarrow z \in x)$$ (Univ Gen)

$$\rightarrow \forall z(z\in x \leftrightarrow z\in y)$$ (Biconditional Intro)

$$\rightarrow x=y$$ (Eq Intro/Axiom of Ext)

Hence:

$$(\forall z (z \notin x) \land \forall z (z \notin y)) \rightarrow x=y$$

So, by universal generalization

$$\forall x \forall y [(\forall z (z \notin x) \land \forall z (z \notin y)) \rightarrow x=y]$$

• Correct........ Jan 25 '20 at 17:21
• Cool, thank you!! Jan 28 '20 at 19:23