The Spectrum of Set Theories

1. One theory or a family of theories

The phrase “set theory” denotes not a single axiomatic system but a family of systems in a common language — the first-order language whose only non-logical symbol is $\in$ (NBG adds a sort of classes). All of them arose in response to one problem: the naive comprehension principle, according to which every property $\varphi(x)$ determines a set $\{x:\varphi(x)\}$, is inconsistent. For $\varphi(x)\equiv x\notin x$ it yields a set $R$ with $R\in R\leftrightarrow R\notin R$ (Russell, 1901). Comprehension must be restricted, and mathematics does not determine the restriction uniquely: the choice expresses a conception of what a set is.

A system results from decisions along several independent axes.

• The iterative conception. Sets are formed in stages from previously formed sets; the universe is the cumulative hierarchy $V=\bigcup_\alpha V_\alpha$, which is never completed and is therefore not itself a set (Zermelo, 1930; Boolos, 1971). ZFC rests on this conception.
• Limitation of size. Only “too large” collections produce contradictions. They can be admitted as objects of a special kind — classes — that are forbidden to be members (von Neumann, 1925). This position is embodied in NBG.
• Well-foundedness. Either membership is well-founded — $x\in x$, cycles $x\in y\in x$ and infinite descending $\in$-chains are excluded (the notion of a well-founded set: Mirimanoff, 1917; the axiom: von Neumann, 1925, and Zermelo, 1930) — or circular objects are legitimate and are given by graphs up to bisimulation (Forti and Honsell, 1983; Aczel, 1988). The second choice leads to ZFA.
• Universality. Everything is a set, the universe included; comprehension is restricted not by size but syntactically — by stratification, which descends from Russell's theory of types (Quine, 1937). This is NF.
• Predicativity. Whether an object may be defined by a quantifier over a totality to which the object itself belongs (Poincaré, 1906; Russell, 1908; Weyl, 1918; Feferman, 1964). The answer separates, in particular, NBG from Morse–Kelley set theory.
• Formal admissibility. For Hilbert, a consistent system of axioms itself secures the existence of its objects. From this standpoint competing systems are compared not by “truth” but by consistency and relative strength.

The table compares four standard systems — ZFC, NBG, ZFA in Aczel's sense, and NF — with two finite $\in$-structures. Let $\Omega$ be a Quine atom, i.e. a set satisfying $\Omega=\{\Omega\}$, and

where in both structures the membership relation consists of the single pair $\Omega\in\Omega$. The complete theories $\mathrm{Th}(M_1)$ and $\mathrm{Th}(M_2)$ make no claim to serve as foundations of mathematics. They serve as control cases: in a finite model every statement is checked directly, which shows which consequence rests on which axiom (§ 4).

2. Comparison table

ZFC — von Neumann's cumulative universe — serves as the reference point; the colour of a label indicates the position of the other systems relative to it.

$\mathcal P(A)$ is the set of all subsets of $A$; $\mathcal P_1(A)=\{\{a\}:a\in A\}$ is the set of singletons; $V_0=\varnothing$, $V_{\alpha+1}=\mathcal P(V_\alpha)$, $V_\lambda=\bigcup_{\alpha<\lambda}V_\alpha$ is the cumulative hierarchy, and $\mathrm{WF}=\bigcup_\alpha V_\alpha$ is the class of well-founded sets; $\langle a,b\rangle=\{\{a\},\{a,b\}\}$ is the Kuratowski pair. $\mathrm{ZFC}^-$ denotes ZFC without the axiom of foundation (Aczel's notation; in another tradition the same symbol denotes ZFC without the power set axiom). The abbreviation ZFA is also used for ZF with urelements (atoms), and it is used in that sense in “Hierarchy of Second-Order Arithmetic Theories”; here $\mathrm{ZFA}=\mathrm{ZFC}^-+\mathrm{AFA}$. The columns $\mathrm{Th}(M_1)$ and $\mathrm{Th}(M_2)$ are analysed in § 4.

3. Comments on the rows

Key prohibition of the language

Each system blocks Russell's paradox by a restriction of a particular kind. In ZFC and ZFA the language admits all formulas, and the restriction concerns the comprehension schema: the collection being defined is separated from an already given set. In two-sorted NBG the prohibition is built into the syntax itself: the atomic formulas are $x\in y$ and $x\in X$, where lower-case variables range over sets and upper-case ones over classes, so a class never stands to the left of $\in$; class comprehension is restricted not by size but by its quantifiers (see “Predicativity”). In one-sorted presentations of NBG the same prohibition is stated as an axiom: every member is a set. In NF the shape of the comprehension formula is restricted — it must be stratifiable — while the range of comprehension is not. $\mathrm{Th}(M_1)$ and $\mathrm{Th}(M_2)$ have no syntactic prohibitions: missing sets are simply absent from the structure.

Status of the universe

In ZFC the existence of a universal set is refuted. If $\forall x\,(x\in v)$, then by the separation schema there is $R=\{x\in v:x\notin x\}$; since $R\in v$, one obtains $R\in R\leftrightarrow R\notin R$. Expressions such as “the class $V$” or “the class $\mathrm{On}$” are admissible in ZFC only as abbreviations of formulas ($x=x$, “$x$ is an ordinal”); such collections are called virtual classes (Quine, 1963).

NBG makes classes objects of a second sort: $V$ and $\mathrm{On}$ exist but are never members. In NF the collection $\{x:x=x\}$ is given by a stratified formula, so $V$ is a set and $V\in V$; the complement $V\setminus A$ of every set $A$ is a set as well. In $M_1$ the universe is $\Omega$ itself; in $M_2$ the domain $\{\varnothing,\Omega\}$ is not an element of the model.

Foundation

The axiom of foundation (regularity): every nonempty set $x$ contains an element $y$ with $y\cap x=\varnothing$. Given the remaining axioms of ZF, it is equivalent to $V=\mathrm{WF}$: every set $x$ has a rank, the least ordinal $\alpha$ with $x\subseteq V_\alpha$. Foundation excludes $x\in x$ (otherwise the set $\{x\}$ would have no $\in$-minimal element), finite cycles $x_0\in x_1\in\dots\in x_n\in x_0$ and infinite descending chains $\dots\in x_2\in x_1\in x_0$. It is also equivalent to the schema of $\in$-induction, which generalizes transfinite induction on the ordinals. The cumulative hierarchy is treated in the summary of chapter C1, “A Mathematician's Paradise”, of the book Mathematics as a Foreign Language; transfinite induction in “On Mathematical Induction”.

Abandoning foundation does not affect mathematics developed inside ZFC: the class $\mathrm{WF}$ remains a model of ZFC and contains all standard objects — numbers, functions, spaces. Only what lies outside $\mathrm{WF}$ changes.

Russell's paradox

The sentence $\neg\exists R\,\forall x\,(x\in R\leftrightarrow x\notin x)$ is a theorem of pure first-order logic: it holds in every structure, $M_1$ and $M_2$ included. The systems differ not in whether they “avoid” the paradox, but in which comprehension principle they retain. Naive comprehension and the passage from it to the hereditarily finite sets are treated in the summary of chapter B2, “The Foundations of Mathematics”, of the same book.

• ZFC and ZFA retain separation (Zermelo's Aussonderung): a property separates a subset only from an already given set. Russell's argument becomes a theorem: for every $A$, the set $\{x\in A:x\notin x\}$ does not belong to $A$, and there is no universal set. Foundation plays no role in the argument, so ZFA behaves exactly like ZFC.
• NBG retains comprehension for classes $\{x:\varphi(x)\}$ where the quantifiers of $\varphi$ range over sets only. The Russell class exists, but it is proper, and only sets are members; under foundation it coincides with $V$.
• NF retains comprehension without any restriction of size, but only for stratifiable formulas.

Cantor's theorem

The diagonal proof uses only separation: for $f\colon A\to\mathcal P(A)$, the set $D=\{x\in A:x\notin f(x)\}$ does not lie in the range of $f$, since $D=f(d)$ implies $d\in D\leftrightarrow d\notin D$. Hence the theorem holds in ZFC and in ZFA regardless of foundation. In NBG it concerns sets; for proper classes there is no analogue: under global choice all proper classes are equinumerous.

In NF the condition $x\notin f(x)$ for $f\colon A\to\mathcal P(A)$ is not stratifiable: $\langle x,y\rangle\in f$ requires $x$ and $y=f(x)$ to have equal types, while $x\notin y$ requires a difference of one. For $f\colon\mathcal P_1(A)\to\mathcal P(A)$ the diagonal condition $a\notin f(\{a\})$ is stratifiable, and the proof goes through: $|\mathcal P_1(A)|<|\mathcal P(A)|$. The map $a\mapsto\{a\}$ is in general not a set in NF, so $|A|$ and $|\mathcal P_1(A)|$ may differ. For $A=V$ one has $\mathcal P(V)=V$ and $|\mathcal P_1(V)|<|V|$: there are strictly fewer singletons than sets.

Predicativity

A definition is impredicative if the object being defined is specified by a quantifier over a totality to which the object itself belongs. Poincaré (1906) and Russell (1908) saw in such definitions the source of the paradoxes (the vicious circle principle); in Weyl's Das Kontinuum (1918) a substantial part of analysis is developed predicatively; the exact limit of predicativity given the natural numbers is the ordinal $\Gamma_0$ (Feferman, 1964; Schütte, 1965).

ZFC is impredicative in two respects. A formula in the separation schema may contain quantifiers over the whole universe, including the set being defined. The power set axiom postulates the totality of all subsets, in particular $\mathcal P(\N)$, as a completed whole. ZFA and NF are impredicative in the same sense; in NF the quantifiers of a stratified formula range over $V$, and $V$ is a set.

NBG is predicative in classes: in class comprehension the quantifiers range over sets only. Consequently the comprehension schema can be replaced by finitely many axioms (NBG is finitely axiomatizable), and NBG is conservative over ZFC: a statement about sets is provable in NBG if and only if it is provable in ZFC. Impredicative class comprehension yields Morse–Kelley set theory (MK), which is strictly stronger: MK proves the consistency of ZFC. Thus classes as objects do not change set theory, whereas impredicative classes strengthen it.

In Feferman's predicativist programme the bulk of scientifically applicable analysis is developed in systems conservative over Peano arithmetic (the system W, 1988). The hierarchy of predicative and impredicative systems is treated in “Hierarchy of Second-Order Arithmetic Theories”, Weyl's predicative analysis in “Levels of Formalization of Mathematical Analysis”.

Ordinals

Following von Neumann (1923), an ordinal is a transitive set strictly well-ordered by $\in$; every ordinal coincides with the set of smaller ordinals: $\alpha=\{\beta:\beta<\alpha\}$. The collection $\mathrm{On}$ of all ordinals cannot be a set (the Burali-Forti paradox): in ZFC it is a virtual class, in NBG a proper class. In ZFA the ordinals are the same as in ZFC, and all of them lie in $\mathrm{WF}$. However, definitions that are equivalent under foundation diverge without it: in ZFA the condition “a transitive set of transitive sets” is also satisfied by the set $\Omega=\{\Omega\}$, which is not an ordinal.

In NF already the transitivity condition $\forall y\in x\;\forall z\in y\;(z\in x)$ is not stratifiable (the types of $x$ and $z$ would have to differ by $1$ and by $2$ simultaneously), so stratified comprehension does not yield a set of von Neumann ordinals. Ordinals are defined after Frege and Russell: an ordinal is the set of all well-orderings isomorphic to a given one; likewise a cardinal is the set of all sets equinumerous with a given one, and the natural number $n$ is the set of all $n$-element sets. The set of all ordinals exists; denote the type of its natural ordering by $\Theta$ (in the NF literature, $\Omega$; here that letter is reserved for the Quine atom).

The Burali-Forti paradox is resolved by the fact that the ordinals smaller than $\Theta$ form a proper initial segment of this ordering and therefore have a type strictly smaller than $\Theta$: the equation “the type of $\{\beta:\beta<\alpha\}$ is $\alpha$”, trivial for von Neumann ordinals, is not stratifiable and fails for $\alpha=\Theta$. Its stratified version is expressed through the operation $T$, which raises the type of an ordering by one level, and yields a descending chain $\Theta>T(\Theta)>T^2(\Theta)>\dots$ that is not a set. Externally the chain is infinite; hence in no model of NF is the ordering of the ordinals well-founded from the standpoint of the metatheory (Rosser and Wang, 1950).

The axiom of choice

In ZFC choice is postulated as a separate axiom; it is independent of the other axioms of ZF (Gödel, 1938; Cohen, 1963). NBG usually adopts global choice — the existence of a class function selecting an element from every nonempty set (Gödel, 1940); this extension is conservative over ZFC (Felgner, 1971). In von Neumann's system (1925) global choice is not postulated separately but follows from the axiom of limitation of size: a class is proper if and only if it can be mapped onto $V$. The same axiom yields separation and replacement, but not the power set axiom: limitation of size by itself does not secure the existence of $\mathcal P(A)$.

AFA is compatible with choice. In NF choice is refuted: the universe cannot be well-ordered (Specker, 1953); as a consequence, NF proves the axiom of infinity. The variant NFU, which admits urelements, is consistent relative to systems considerably weaker than ZFC and compatible with choice (Jensen, 1969). The consistency of NF itself had remained open since 1937; the proof by Holmes and Wilshaw constructs a model of tangled type theory TTT, whose consistency is equivalent to that of NF, and has been verified in the Lean proof assistant (2024).

Basic axioms

NF differs from the other infinite systems in separation: from a set $A$ only a subset defined by a stratifiable condition can be separated; thus $\{x\in V:x\notin x\}$ does not exist. In return NF contains sets impossible in ZFC: $V$, complements, the set of all ordinals, the set of all cardinals. The basic axioms in $M_1$ and $M_2$ are checked in § 4.

4. The finite models $M_1$ and $M_2$

The models $M_1=\langle\{\Omega\};\in\rangle$ and $M_2=\langle\{\varnothing,\Omega\};\in\rangle$, where $\Omega=\{\Omega\}$, are checked by exhaustive search: in a finite structure every subset of the domain is definable with parameters, so the separation and replacement schemas reduce to finitely many checks.

Russell's dilemma in miniature. Separation and a universal set are incompatible: from separation Russell's argument derives $\{x\in A:x\notin x\}\notin A$ for every $A$. The models $M_1$ and $M_2$ realize the two horns of this dilemma. In $M_1$ the universal set $\Omega$ exists, while separation fails: $\{x\in\Omega:x\notin x\}=\varnothing$ is absent from the model. In $M_2$ separation holds, and there is no universal set: $\{x\in\Omega:x\notin x\}=\varnothing\notin\Omega$. The same choice, at full scale, separates ZFC (full separation, no universe) from NF (a universe, separation restricted by stratification).

Cantor's theorem. In $M_1$ the Kuratowski pair degenerates: $\langle\Omega,\Omega\rangle=\{\{\Omega\},\{\Omega,\Omega\}\}=\{\Omega\}=\Omega$. Hence $\Omega=\{\langle\Omega,\Omega\rangle\}$ is a function with domain $\Omega$, and since $\mathcal P(\Omega)=\Omega$, it maps $\Omega$ bijectively onto $\mathcal P(\Omega)$: Cantor's theorem fails. The diagonal set $\{x\in\Omega:x\notin f(x)\}$ would be empty and is absent from the model — the counterexample rests on the failure of separation. In $M_2$ there are no power sets: $\mathcal P(\varnothing)=\{\varnothing\}$ and $\mathcal P(\Omega)=\{\varnothing,\Omega\}$ are not elements of the model, so the formulation $|A|<|\mathcal P(A)|$ is vacuous. The formulation without power sets — for every function $f$ with domain $A$ there is $B\subseteq A$ not in the range of $f$ — holds: the only functions in $M_2$ are $\varnothing$ and $\Omega$, and $B=\varnothing$ works for $f=\Omega$. This is again a consequence of separation.

Foundation and choice. In both models the set $\Omega=\{\Omega\}$ has no $\in$-minimal element. It is essential that the set $\{\Omega\}$ be present in the model: without the pairing axiom, regularity does not imply $x\notin x$. If $\Omega$ is replaced by an element $\Omega'=\{\varnothing,\Omega'\}$, then regularity holds in the structure $\langle\{\varnothing,\Omega'\};\in\rangle$ ($\varnothing$ is an $\in$-minimal element of $\Omega'$), although $\Omega'\in\Omega'$. Choice in $M_1$ and $M_2$ is trivial: the only nonempty family of nonempty sets is $\Omega$, and $\Omega=\{\langle\Omega,\Omega\rangle\}$ is its choice function.

Ordinals and infinity. In $M_1$ there are no ordinals: $\Omega$ is transitive, but $\Omega\in\Omega$ violates the strictness of the order, and $\varnothing$ is absent. In $M_2$ the only ordinal is $0=\varnothing$; already $1=\{\varnothing\}$ is absent. The standard axiom of infinity fails in both models. However, the formulation “there is a nonempty set without an $\in$-maximal element”, $\exists x\,(\exists y\,(y\in x)\wedge\forall y\in x\;\exists z\in x\;(y\in z))$, which is equivalent to the standard one given the remaining axioms of ZF, holds in both models, with $\Omega$ as a witness. Without foundation, formulations equivalent in ZF cease to be equivalent.

5. Positions: Zermelo, Hilbert, von Neumann, Quine, Aczel, Feferman

The columns of the table are consequences of several philosophical positions on the nature of sets and on the criteria of admissibility of mathematical objects. Each card indicates the columns and rows of the table in which the corresponding position manifests itself.

The vicious circle principle was formulated by Poincaré (1906) and Russell (1908); Russell's ramified theory of types is a common ancestor of the predicativist programme and, through the simple theory of types, of NF. The final form of NBG is due to Bernays and Gödel; the central results on NF and NFU to Specker (1953) and Jensen (1969); the analysis of the iterative conception as a justification of the ZFC axioms to Boolos (1971).

6. Beyond the table

• Z and ZC. Zermelo's 1908 system, without replacement. $V_{\omega+\omega}$ is a model of it, so Z does not prove the existence of the ordinal $\omega+\omega$, let alone of $\aleph_\omega$.
• MK. Morse–Kelley set theory: NBG with impredicative class comprehension; proves the consistency of ZFC.
• KP. Kripke–Platek set theory: no power set axiom, separation and collection only for formulas with bounded quantifiers; the basis of the theory of admissible sets (Barwise, 1975).
• ZF with urelements. Atoms are objects without elements distinct from $\varnothing$; the Fraenkel–Mostowski permutation models prove the independence of the axiom of choice in this setting.
• NFU. NF with urelements: consistent, compatible with choice and infinity (Jensen, 1969).
• CZF and IZF. Constructive set theories with intuitionistic logic; CZF (Aczel, 1978) has no power set axiom and is interpreted in Martin-Löf type theory.

7. References

1. E. Zermelo, Untersuchungen über die Grundlagen der Mengenlehre I, Math. Ann. 65 (1908), 261–281.
2. E. Zermelo, Über Grenzzahlen und Mengenbereiche, Fund. Math. 16 (1930), 29–47.
3. D. Mirimanoff, Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles, Enseign. Math. 19 (1917), 37–52.
4. J. von Neumann, Eine Axiomatisierung der Mengenlehre, J. reine angew. Math. 154 (1925), 219–240.
5. D. Hilbert, Über das Unendliche, Math. Ann. 95 (1926), 161–190.
6. W. V. Quine, New foundations for mathematical logic, Amer. Math. Monthly 44 (1937), 70–80.
7. J. B. Rosser, H. Wang, Non-standard models for formal logics, J. Symbolic Logic 15 (1950), 113–129.
8. E. Specker, The axiom of choice in Quine's New Foundations for mathematical logic, Proc. Nat. Acad. Sci. USA 39 (1953), 972–975.
9. W. V. Quine, Set Theory and Its Logic, Harvard University Press, Cambridge, MA, 1963.
10. S. Feferman, Systems of predicative analysis, J. Symbolic Logic 29 (1964), 1–30.
11. R. B. Jensen, On the consistency of a slight (?) modification of Quine's New Foundations, Synthese 19 (1969), 250–263.
12. G. Boolos, The iterative conception of set, J. Philos. 68 (1971), 215–231.
13. U. Felgner, Comparison of the axioms of local and universal choice, Fund. Math. 71 (1971), 43–62.
14. M. Forti, F. Honsell, Set theory with free construction principles, Ann. Sc. Norm. Super. Pisa Cl. Sci. (4) 10 (1983), 493–522.
15. P. Aczel, Non-Well-Founded Sets, CSLI Lecture Notes 14, CSLI, Stanford, 1988.
16. S. Feferman, Weyl vindicated: Das Kontinuum seventy years later (1988), in: S. Feferman, In the Light of Logic, Oxford University Press, New York, 1998, 249–283.
17. M. R. Holmes, S. Wilshaw, NF is consistent, arXiv:1503.01406.