In axiomatic set theory, the axiom of empty set 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.
Formal statement
In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:

\exists x\, \forall y\, \lnot (y \in x)
or in words:

There is a set such that no set is a member of it.
Interpretation
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:

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.
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. That said, 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.
In many formulations of firstorder predicate logic, the existence of at least one object is always guaranteed. If the axiomatization of set theory is formulated in such a logical system with the axiom schema of separation as axioms, and if the theory makes no distinction between sets and other kinds of objects (which holds for ZF, KP, and similar theories), then the existence of the empty set is a theorem.
If separation is not postulated as an axiom schema, but derived as a theorem schema from the schema of replacement (as is sometimes done), the situation is more complicated, and depends on the exact formulation of the replacement schema. The formulation used in the axiom schema of replacement article only allows to construct the image F[a] when a is contained in the domain of the class function F; then the derivation of separation requires the axiom of empty set. On the other hand, the constraint of totality of F is often dropped from the replacement schema, in which case it implies the separation schema without using the axiom of empty set (or any other axiom for that matter).
References

Burgess, John, 2005. Fixing Frege. Princeton Univ. Press.

Paul Halmos, Naive set theory. Princeton, NJ: D. Van Nostrand Company, 1960. Reprinted by SpringerVerlag, New York, 1974. ISBN 0387900926 (SpringerVerlag edition).

Jech, Thomas, 2003. Set Theory: The Third Millennium Edition, Revised and Expanded. Springer. ISBN 3540440852.

Kunen, Kenneth, 1980. Set Theory: An Introduction to Independence Proofs. Elsevier. ISBN 0444868399.
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.