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...

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


$$(\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]$$

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.