Equivalence of Definitions of Empty Set

From ProofWiki
Jump to navigation Jump to search


The following definitions of the concept of Empty Set are equivalent:

Formulation 1

There exists a set that has no elements:

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

Formulation 2

There exists a set for which membership leads to a contradiction:

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


Formulation 2 implies Formulation 1

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


Formulation 1 implies Formulation 2

\(\text {(1)}: \quad\) \(\ds \) \(\) \(\ds \forall y: \paren {\neg \paren {y \in x} }\)
\(\text {(2)}: \quad\) \(\ds \) \(\) \(\ds \forall y: \neg \paren {y \in x} \land \paren {y \in x} \implies y \ne y\) Rule of Explosion
\(\text {(3)}: \quad\) \(\ds \) \(\) \(\ds \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\) \(\ds \) \(\) \(\ds \forall y: \paren {y \in x \implies y \ne y}\) Modus Ponendo Ponens, from $(1)$ and $(3)$