===== Empty set =====
==== Set ====
| @#FFBB00: definiendum | @#FFBB00: $x\in\emptyset$ |
| @#55EE55: postulate   | @#55EE55: $\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 [[http://en.wikipedia.org/wiki/Axiom_of_empty_set|axiom of empty set (Wikipedia)]].

Uniqueness is discussed, for example, in 
[[https://proofwiki.org/wiki/Empty_Set_is_Unique|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$.

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Empty_set|Empty set]], 
[[http://en.wikipedia.org/wiki/Axiom_of_empty_set|Axiom of empty set (Wikipedia)]]

Proof Wiki: 
[[https://proofwiki.org/wiki/Empty_Set_is_Unique|Empty Set is Unique (Proof Wiki)]]

-----
=== Requirements ===
[[Set theory]]
=== Subset of ===
[[First infinite von Neumann ordinal]]