The existence of the empty set is an axiom of ZFC or not?

In short, we do not need to adopt this as an axiom. But...

If there are sets at all, the axiom of subsets tells us that there is an empty set: If $x$ is a set, then $\{y\in x\mid y\ne y\}$ is a set, and is empty, since there are no elements $y$ of $x$ for which $y\ne y$. The axiom of extensionality then tells us that there is only one such empty set.

So, the issue is whether we can prove that there are any sets. The axiom of infinity tells us that there is a set (which is infinite, or inductive, or whatever formalization you use). But this seems like a terrible overkill to check that there are sets, to postulate that there are infinitely many.

Some people prefer to have an axiom that states that there are sets. Of course, some people then just prefer to have an axiom that states that there is an empty set, so we at once have that there are sets, and avoid having to apply comprehension to check that the empty set exists.

Other people adopt a formalization of first order logic in which we can prove that there are sets. More carefully, most formalizations of logic (certainly the one I prefer) prove as a theorem that the universe of discourse is nonempty. In the context of set theory, this means "there are sets". This is pure logic, before we get to the axioms of set theory. Under this approach, we do not need the axiom that states that there are sets, and the existence of the empty set can be established as explained above.

(The logic proof that there are sets is not particularly illuminating or philosophically significant. Usually, one of the axioms of first order logic is that $\forall x\,(x=x)$. If $\exists x\,(x=x)$ --the formal statement corresponding to "there are sets"-- is false, then $\forall x\,(x\ne x)$. Instantiating, we obtain $x\ne x$, and instantiating the axiom $\forall x\,(x=x)$ we obtain $x=x$, and one of these conclusions is the negation of the other, which is a contradiction. This is not particularly illuminating, because of course we choose our logical axioms and rules of instantiation so that this silly argument can go through, it is not a deep result, and probably we do not gain much insight from it.)

It turns out that yet some others prefer to allow the possibility that there are empty universes of discourse, so their formalization of first order logic is slightly different, and in this case, we have to adopt some axiom to conclude that there is at least one set.

At the end of the day, this is considered a minor matter, more an issue of personal taste than a mathematical question.


Whether it's listed as an axiom or not depends on the temperament of the author.

In most formalizations of first-order logic (the underlying logic behind ZFC set theory), the formula "there exists something": $$\exists x.(x\in x\lor x\notin x)$$ is a logical tautology -- that is, it is provable without using any proper axioms at all. (Semantically, the usual first-order logic assumes that the universe of the theory is implicitly non-empty). From there we can easily produce an empty set by the subset axiom: $$ \varnothing = \{ y \in x \mid y\in y\land y\notin y \}$$ and this empty set is unique by the Axiom of Extensionality.

Many authors, however, think it makes for clearer exposition to list the existence of an empty set as an explicit axiom rather than depend on subtleties of the underlying logic.

Even in logics where the universe is allowed to be empty (and $\exists x.\mathit true$ is not a logical tautology) we could in principle make do with the Axiom of Infinity, which also (in some of its possible formulations) asserts the existence of a set with certain properties without depending on any pre-existing sets. Then, as before, the empty set can be constructed as $\{ y \in \omega \mid y\in y \land y\notin y\}$.

However, this latter option is inconvenient in practice because there are interesting things to say about "ZFC without the Axiom of Infinity", and it would be cumbersome (and less striking) to have to speak about "ZFC without the Axiom of Infinity, but with an added Null Set axiom" when stating those results.


There are a number of elementarily equivalent axiomatizations of ZFC (in the sense that the proofs of equivalence involve only elementary logical considerations). As you note, on some axiomatizations, the existence of an empty set is an axiom (with other axioms proving uniqueness), on other axiomatizations the existence of the empty set is a theorem. There is nothing deep going on here!