Equivalence of Definitions of Empty Set

From ProofWiki
Jump to navigation Jump to search


Theorem

The two axiomatic definitions of the empty set:

$\exists x: \forall y: \paren {\neg \paren {y \in x} }$

and

$\exists x: \forall y \in x: y \ne y$

are logically equivalent.


Proof

Definition 2 implies Definition 1

\(\text {(1)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \forall y: y = y\) Equality is Reflexive
\(\text {(2)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \neg \exists y: y \ne y\) From $(1)$
\(\text {(3)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle x := \set { {y: y \ne y} }\)
\(\text {(4)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \neg \exists y: y \in x\) From $(2)$ and $(3)$

$\Box$


Definition 1 implies Definition 2

\(\text {(1)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \forall y: \paren {\neg \paren {y \in x} }\)
\(\text {(2)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \forall y: \neg \paren {y \in x} \land \paren {y \in x} \implies y \ne y\) Rule of Explosion
\(\text {(3)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \forall y: \paren {\neg \paren {y \in x} \implies \paren {y \in x \implies y \ne y} }\) Rule of Exportation, from $(2)$
\(\text {(4)}: \quad\) \(\displaystyle \) \(\) \(\displaystyle \forall y: \paren {y \in x \implies y \ne y}\) Modus Ponendo Ponens, from $(1)$ and $(3)$


Sources