nLab ZFC





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



The most commonly accepted standard foundation of mathematics today is a material set theory commonly known as Zermelo–Fraenkel set theory with the axiom of choice or ZFCZFC for short. There are many variations on that theory (including constructive and class-based versions, which are also discussed here).

Accompanying ZFC, especially taking into account the axiom of foundation, is a picture (or ‘ontology’) of material sets forming a cumulative hierarchy organized by an ordinal-valued rank function. This picture (sometimes referred to as the ‘iterative conception’) considers sets as generated by starting at bottom with the empty set and building to higher ranks by applying a power set operation to get to a next successor ordinal rank, and taking unions to get to limit ordinal ranks. This iterative conception finds alternative expression in algebraic set theory.


The first version was developed by Ernst Zermelo in 1908; in 1922, Abraham Fraenkel and Thoralf Skolem independently proposed a precise first-order version with the axiom of replacement; von Neumann added the axiom of foundation in 1925. All of these versions included the axiom of choice, but this was considered controversial for some time; one has merely ZFZF if it is taken out.

ZFCZFC is similar to the class theories NBG (due to John von Neumann, Paul Bernays, and Kurt Gödel) and MK (due to Anthony Morse and John Kelley). The former is a conservative, finitely axiomatisable extension of ZFCZFC, while the latter is stronger and cannot be finitely axiomatised (although a conservative extension involving meta-classes could be).

Contemporary set theorists often accept additional large cardinal axioms, which can greatly increase the strength of ZFCZFC, far beyond even MKMK. Other additional axioms which are sometimes added are the axiom of determinacy (or various weaker versions of it) or the axiom of constructibility. There are also weaker variants of ZFCZFC, especially for constructive and predicative mathematics. Then there are alternatives on a different basis, notably NFU (a very impredicative material set theory with a set of all sets) and ETCS (a structural set theory).

(The source for this history, especially the dates, is mostly the English Wikipedia.)


ZFCZFC is a simply typed first-order material set theory, with a single type VV called the cumulative hierarchy and a binary membership predicate \in on VV. Every term of VV in standard ZFCZFC is a pure set, which we will call simply a set. A set aa is said to belong to, be in, be a member of, or be an element of a set bb if aba \in b, and set bb is said to have the member aa.

There are also variations of ZFC with non-set terms such as urelements and classes. Urelements may be distinguished from sets and classes since they have no elements (although the empty set also has no elements); sets are usually those classes that are themselves elements (members) of sets. Urelements are also called atoms, and ZFZF with atoms included is sometimes called ZFA or ZFUZFU.

  1. Extensionality: If two sets have the same members, then they are equal and themselves members of the same sets. See axiom of extensionality for variations, such as whether this is taken as a definition or an axiomatisation of equality of sets, and how the condition might be strengthened if (10) is left out.

  2. Null Set: There is an empty set: a set \empty with no elements. By (1), it follows that this set is unique; by even the weakest version of (5), it is enough to state the existence of some set. (Analogous remarks apply to axioms (3), (4), (6), (7), and (8), except when (5) is omitted and (4) and (6) are needed to derive it.)

  3. Pairing: If aa and bb are sets, then there is a set {a,b}\{a,b\}, the unordered pairing of aa and bb, whose elements are precisely those sets equal to aa or bb. Between them, (2) and (3) form a nullary/binary pair; the unary version follows from (3), since {a}={a,a}\{a\} = \{a,a\} by (1). The higher finitary versions rely also on (4) (with {a,b,c}={a}{b,c}\{a,b,c\} = \{a\} \cup \{b,c\}, etc), so they should probably be stated explicitly as an axiom scheme if (4) is omitted (but nobody seems to do that).

  4. Union: If 𝒞\mathcal{C} is a set, then there is a set 𝒞\bigcup \mathcal{C}, the union of 𝒞\mathcal{C}, whose elements are precisely the elements of the elements of 𝒞\mathcal{C}. It is normal to write ABA \cup B for {A,B}\bigcup \{A,B\}, etc, ABCA \cup B \cup C for {A,B,C}\bigcup \{A,B,C\}, etc. Note that {A}=A\bigcup \{A\} = A and =\bigcup \empty = \empty (using (1) to prove these results), so no special notation is needed for these.

  5. Separation/Specification/Comprehension: Given any predicate ϕ[x]\phi[x] in the language of set theory with the chosen free variable xx of type VV, if UU is a set, then there is a set {xU|ϕ[x]}\{x \in U \;|\; \phi[x]\}, the subset of UU given by ϕ\phi, whose elements are precisely those elements xx of UU such that ϕ[x]\phi[x] holds. There are many variations, from Bounded Separation to Full Comprehension, which we should probably describe at axiom of separation; the version listed here is Full Separation. This is an axiom scheme, but it can be made a single axiom in NBGNBG (but not completely in MKMK). Note that (5) follows from (4) and (6) using classical logic, so it is often left out, but it must be included in intuitionistic variations, variations where (6) is omitted or weakened (or where (4) is omitted or weakened, in principle, although that never happens in practice), and variations where (5) itself is strengthened.

  6. Replacement/Collection: Given a predicate ψ[x,Y]\psi[x,Y] with the chosen free variables xx and YY of type VV, if UU is a set and if for every xx in UU there is a unique YY such that ψ[x,Y]\psi[x,Y] holds, then there is set {ιY.ψ[x,Y]|xU}\{\iota\,Y.\;\psi[x,Y] \;|\; x \in U\}, the image of UU under ψ\psi, whose elements are precisely those sets YY such that there is an element xx of UU such that ψ[x,Y]\psi[x,Y] holds; if Ψ[x]\Psi[x] is a defined term, then we write {Ψ[x]|xU}\{\Psi[x] \;|\; x \in U\} for {ιY.Y=Ψ[x]|xU}\{\iota\,Y.\; Y = \Psi[x] \;|\; x \in U\}. Again there are many variations, from Weak Replacement to Strong Collection, which we should probably describe at axiom of replacement; the one described here is Replacement. This is also an axiom scheme, but it can be made into a single axiom in both NBGNBG and MKMK. One could combine this with (5) to produce {ιY.ψ[x,Y]|xU|ϕ[x]}\{\iota\,Y.\;\psi[x,Y] \;|\; x \in U \;|\; \phi[x]\}, but nobody seems to do this.

  7. Power Sets: If UU is a set, then there is a set 𝒫U\mathcal{P}U, the power set of UU, whose elements are precisely the subsets of UU, that is the sets AA whose elements are all elements of UU. When using intuitionistic logic, it is possible to accept only a weak version of this, such as Subset Collection or (even weaker) Exponentiation. But in classical logic, Power Sets follows from Exponentiation and the weakest form of (5).

  8. Infinity: There is a set ω\omega of finite ordinals as pure sets. Normally one states that ω\empty \in \omega and a{a}ωa \cup \{a\} \in \omega whenever aωa \in \omega, although variations are possible. Using any but the weakest version of (6), it is enough to state that there is a set satisfying Peano's axioms of natural numbers, or even any Dedekind-infinite set. It seems to be uncommon to incorporate (2) into (8), but in principle (8) implies (2).

  9. Choice: If 𝒞\mathcal{C} is a set of pairwise disjoint sets, each of which has an element, then there is a set with exactly one element from each element of 𝒞\mathcal{C}. Note that this set is not unique, nor can we construct a canonical version which is, so we do not give it any name or notation. This version is the simplest to state in the language of ZFCZFC; see axiom of choice for further discussion and weak versions. It is possible to incorporate (9) into (5) or (6), but this seems to be rare.

  10. Foundation/Regularity/Induction: Given a formula ϕ\phi with a chosen free variable XX of type VV, if ϕ\phi holds whenever ϕ[a/X]\phi[a/X] holds for every aXa \in X, then ϕ\phi holds absolutely. For variations (including the axiom of anti-foundation), see axiom of foundation. This axiom scheme can be made into a single axiom even in ZFCZFC itself (although not in versions with intuitionistic logic; in that case it can be made a single axiom only in a class theory).


Zermelo's original version consists of axioms (1–5) and (7–9), in a somewhat imprecise form (which affects the interpretation of 5) of higher-order classical logic.

The modern ZFZF consists of (1–8) and (10), using first-order classical logic, the strongest form of (6) (that is, Strong Collection, although the standard Replacement is sufficient with classical logic), and the strongest form of (5) possible using only sets and not classes (Full Separation). Since Full Separation follows from Replacement with classical logic, it is often omitted from the list of axioms.

ZFCZFC adds (9) and is thus the strongest version without classes or additional axioms. The version originally formulated by Fraenkel and Skolem did not include (10), although the three founders all eventually accepted it.

It is common to take Zermelo set theory (Z\mathrm{Z}) to be ZFZF without (6), although Zermelo never accepted the first-order formulation, and his axioms did not include the Axiom of Foundation (10). Note that the weakest form (Weak Replacement) of (6) follows from (7) and (5), so it holds even in Z\mathrm{Z}.

Another variant is bounded Zermelo set theory (BZBZ), which is like Z\mathrm{Z} but with only Bounded Separation; this is of interest to category theorists because BZCBZC is equivalent to ETCS.

Constructive versions

See also constructive set theory.

The most well-known foundations for constructive mathematics through material set theory are Peter Aczel's constructive Zermelo–Fraenkel set theory (CZFCZF) and John Myhill's intuitionistic Zermelo–Fraenkel set theory (IZFIZF).

CZFCZF uses axioms (1–8) and (10), usually weak forms, in intuitionistic logic; specifically, it uses Bounded Separation for (5), Strong Collection for (6), and an intermediate (Subset Collection) form of (7). IZFIZF is simliar, but it uses Full Separation for (5) and the full strength of (7); Myhill's original version uses only Replacement for (6), but Collection (equivalent to Strong Collection using Full Separation) is standard now.

Note that adding (9) to IZFIZF implies excluded middle and so makes ZFCZFC. However, some authors like to include a weak form of (9), such as dependent choice or COSHEP.

Mike Shulman's survey of material and structural set theories (Shulman 2018) takes CPZ CPZ^{\circlearrowleft-} as the most basic form; it consists of (1–4) and the weakest versions (Bounded Separation and Weak Replacement) of (5&6) in intuitionistic logic. Adding (10) gives CPZ CPZ^{-}, adding (8) gives CPZ CPZ^{\circlearrowleft}, and adding both gives CPZCPZ, constructive pre-Zermelo set theory. Shulman gives systematic notation for other versions, which includes those (constructive and classical) listed above.

Myhill has another version, constructive set theory (CSTCST); this consists of (1–4), Bounded Separation for (5), Replacement for (6), the weakest (Exponentiation) form of (7), (8), and a weak version (Dependent Choice) of (9). It also uses a variation of the language, with urelements for natural numbers; note that the existence of ω\omega still follows using (6). This classifies CSTCST as CΠZF +DC\mathrm{C}{\Pi}ZF^{\circlearrowleft} + DC in Shulman's system if one ignores the use of urelements and strengthens Replacement to Strong Collection.

Class theories

Morse–Kelley class theory (MKMK) features both sets and proper classes. This allows it to strengthen (5) to Full Comprehension, since ϕ\phi can include quantification over classes; the same holds in (6) and (10), although this does not add any additional strength.

Von Neumann–Bernays–Gödel class theory (NBGNBG) uses the same language as MKMK, but it still uses only Full Separation for (5). This makes it conservative over ZFCZFC and also allows for a finite axiomatisation; we replace the formulas in (5) and (6) with classes, and add some special cases of (5) for subclasses, one for each logical connective. (It is provable that plain ZFZF, if consistent, cannot be finitely axiomatized in its own first-order language; NBGNBG escapes this conclusion by extending the language with the notion of classes.)

One can also rework all of the weak versions of set theory above into a class theory like NBGNBG, which is conservative over the original set theory. One can also use a class theory like MKMK, although this destroys any attempt to use a weak version of (5).

Large cardinals

One often adds axioms for large cardinals to ZFCZFC. Even (8) can be seen as a large cardinal axiom, stating that 0\aleph_0 exists. These additional axioms are most commonly studied in the context of a material set theory, but they work just as well in a structural set theory.

Note that adding an inaccessible cardinal (commonly considered the smallest sort of large cardinal) to ZFCZFC is already stronger than MKMK: given an inaccessible cardinal κ\kappa, one can interpret the sets and classes in MKMK as the sets in V κV_\kappa and V κ+1V_{\kappa+1}, respectively. Of course, one can add a large cardinal to MKMK to get something even stronger.

It is often convenient to assume that one always has more large cardinals when necessary. You cannot say this in an absolute sense, but you can adopt the axiom that every set belongs to some Grothendieck universe. Adding this axiom to ZFCZFC makes Tarski-Grothendieck set theory (TGTG). This is not the last word, however; you can make it stronger by adding classes in the style of MKMK, or even adding a cardinal which is inaccessible from TGTG. In fact, we have barely begun the large cardinals known to modern set theory!

Miscellaneous variations

The axiom of constructibility, usually notated “V=LV = L”, is a very strong axiom that can be added to ZFZF; it asserts that all sets belong to the constructible universe LL, which can be “constructed” in a definable way through a transfinite procedure. This notion of “constructible” should not be confused with constructive mathematics; for instance, V=LV = L implies the axiom of choice and thus also excluded middle even with intuitionistic logic. V=LV = L also implies the generalized continuum hypothesis (GCHGCH), which is how Gödel originally proved that GCHGCH was consistent with ZFCZFC. However, it is incompatible with the sufficiently large cardinals: the existence of a measurable cardinal implies that VLV \neq L. Most contemporary set theorists do not regard V=LV = L as potentially “true.”

The axiom of determinacy (ADAD) is another axiom that can be added to ZFZF; it asserts that a certain class of infinite game?s is determined (one player or the other has a winning strategy). ADAD is inconsistent with the full axiom of choice, although it is consistent with dependent choice. A weaker form of ADAD called “projective determinacy” is consistent with ACAC and is equiconsistent with certain large cardinal assertions.

The GCHGCH itself, or its negation, could also be regarded as an additional axiom that can be added to ZFZF. Many set theorists would prefer to find a more “natural” axiom, such as a large cardinal axiom, which implies either GCHGCH or its negation. The equiconsistency of projective determinacy with a large cardinal assertion can be regarded as a step in this direction.

Relation to structural set theories

The structural set theory ETCS is equivalent to BZCBZC in that the category of sets in that theory satisfies ETCSETCS while the well-founded pure sets in ETCSETCS satisfy BZCBZC. This uses (1–4), Bounded Separation for (5), and (7–10), with Weak Replacement following from (5) and (7).

Mike Shulman's SEARC is equivalent to ZFCZFC in the same way. SEARSEAR, which lacks the axiom of choice, is equivalent to ZF ZF^{\circlearrowleft}, which is ZFZF without (10), in a weaker sense of equivalence.

Shulman 2018 is an extensive survey of variations of ZFCZFC and variations of ETCSETCS (mostly weak ones), showing how these correspond.


Zermelo’s axiomatisation grew out of his reflections on his proofs of the well-ordering theorem (1904/08) and was published in

  • Ernst Zermelo, Untersuchungen über die Grundlagen der Mengenlehre I , Math. Ann. 65 (1908) pp.261-81. (gdz)

English versions of the early key texts on set theory by Zermelo, Fraenkel, Skolem, von Neumann et al. can be found in

  • J. van Heijenoort, From Frege to Gödel - A Sourcebook in Mathematical Logic 1879-1931 , Harvard UP 1967.

There are many texts which discuss ZFC and the cumulative hierarchy from a traditional (material) set-theoretic perspective. A good example is

  • Kenneth Kunen, Set Theory: An Introduction to Independence Proofs, Studies in Logic and the Foundations of Mathematics Vol. 102 (2006), Elsevier.

A classification of axioms of variants of ZFCZFC, with an eye towards corresponding structural set theories, is

Last revised on May 9, 2023 at 11:24:47. See the history of this page for a list of all contributions to it.