## Empty set

### Set

definiendum | $x\in\emptyset$ |

postulate | $\bot$ |

Here we extend our language by the symbol $\emptyset$ (sometimes $\varnothing$ or $\{\}$ is used also), denoting $\{x\mid \bot\}$, i.e.

$\emptyset\equiv\{x\mid \bot\}$

This is sensible in our set theory if the proposition

$\exists! y.\,y=\{x\mid \bot\}$

holds, which really is an abbreviation for

$\exists! y.\,\forall x.\,\left(x\in y\Leftrightarrow \bot\right)$

and where $\exists! y.\ \phi(y)$ has been defined as $\exists y.\ \forall z.\ (\phi(z) \Leftrightarrow y=z)$, see Predicate logic.

In words: “There exists a unique set $y$, such that it having any elements $x$ would be absurd.”

#### Discussion

So is it true? Does our set theory permit the existence of such a set $y$?

As $\bot\implies P$ is $\top$ for any $P$ and as $Q\land\top$ is logically equivalent to $Q$, the above is logically equivalent to

$\exists! y.\,\forall x.\,\left(x\in y\implies \bot\right)$

which is

$\exists! y.\,\forall x.\,\neg(x\in y)$

or

$\exists! y.\,\nexists x.\,x\in y$

Apart from the exclamation mark, this is exactly the axiom of empty set (Wikipedia).

Uniqueness is discussed, for example, in Empty Set is Unique (Proof Wiki). It requires judgements of equality of sets, which is proven via the axiom of extensionality.

##### Remark

We could also avoid the symbol $\bot$ and use the predicate $x\neq x$.