nLab
ZFC

Contents

Idea

The commonly accepted standard foundation of mathematics today is a material set theory, ZFCZFC or Zermelo–Fraenkel set theory with the axiom of choice.

History

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 MKMK (due to Anthony Morse? and John Kelley, see Morse-Kelley set theory). The former is a conservative, finitely axiomatisable extension of ZFCZFC, while the latter is stronger and cannot be finitely axiomatised (without introducing meta-classes or something).

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 NFUNFU (a very impredicative material set theory) and ETCS (a structural set theory).

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

Axioms

ZFCZFC is a material set theory, based on a global binary membership predicate \in. Everything in standard ZFCZFC is a pure set, which we will call simply a set; but there are also variations with 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 most of the other axioms.)

  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).

  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. Besides its own power, this gives ternary and higher versions of (3), with {a,b,c}={a}{b,c}\{a,b,c\} = \{a\} \cup \{b,c\}, etc.

  5. Separation/Specification/Comprehension: Given any predicate ϕ[x]\phi[x] in the language of set theory with the chosen free variable shown, 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. 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, except in weak or intuitionistic versions.

  6. Replacement/Collection: Given a predicate ψ[x,Y]\psi[x,Y] with the chosen free variables shown, 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. This 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.

  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, each of whose elements 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, 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 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).

Variations

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; 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

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 unfinished survey of material and structural set theories 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).

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.

Revised on March 9, 2014 09:07:45 by Toby Bartels (98.23.139.218)