In axiomatic set theory, the axiom of empty set, also called the axiom of null set and the axiom of existence, is a statement that asserts the existence of a set with no elements. It is an axiom of Kripke–Platek set theory and the variant of general set theory that Burgess (2005) calls "ST," and a demonstrable truth in Zermelo set theory and Zermelo–Fraenkel set theory, with or without the axiom of choice.

In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:

Or, alternatively, ${\displaystyle \exists x\,\lnot \exists y\,(y\in x)}$.

In words:

We can use the axiom of extensionality to show that there is only one empty set. Since it is unique we can name it. It is called the empty set (denoted by { } or ∅). The axiom, stated in natural language, is in essence:

This formula is a theorem and considered true in every version of set theory. The only controversy is over how it should be justified: by making it an axiom; by deriving it from a set-existence axiom (or logic) and the axiom of separation; by deriving it from the axiom of infinity; or some other method.

In some formulations of ZF, the axiom of empty set is actually repeated in the axiom of infinity. However, there are other formulations of that axiom that do not presuppose the existence of an empty set. The ZF axioms can also be written using a constant symbol representing the empty set; then the axiom of infinity uses this symbol 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 may still be required. However, any axiom of set theory or logic that implies the existence of any set will imply the existence of the empty set, if one has the axiom schema of separation. This is true, since the empty set is a subset of any set consisting of those elements that satisfy a contradictory formula.