Axiom of empty set

In the formal language of the Zermelo-Frankel axioms, the axiom reads:

∃ A, ∀ B, ¬(B ∈ A);

There is a set A such that, given any set B, B is not a member of A.

We can use the axiom of extension to show that this set A is unique. We call the set A the empty set, and denote it {}. Thus the essence of the axiom is:

An empty set exists.

The axiom of empty set is generally considered uncontroversial, and it or an equivalent appears in just about any alternative axiomatisation of set theory.

The axiom of empty set may also be seen as a special case of a generalisation of the axiom of pairing.

In some formulations of ZF, the axiom of empty set is actually repeated in the axiom of infinity. On the other hand, there are other formulations of that axiom that don't presuppose the existence of an empty set. Also, the ZF axioms can also written using a constant predicate[?] representing the empty set; then the axiom of infinity uses this predicate without requiring it to be empty, while the axiom of empty set is needed to state that it is in fact empty. Furthermore, one sometimes considers set theories in which there are no infinite sets, and then the axiom of empty set will still be required. That said, any axiom that states the existence of any set will imply the axiom of empty set, using the axiom schema of separation.