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, IST a standardness predicate). 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). The derivation does not use the meaning of the relation $\in$ and goes through for every binary predicate (§ 6). 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.
• Standardness. The language is extended by a unary predicate $\mathrm{st}(x)$, “$x$ is standard”, while the separation and replacement schemas are retained only for formulas of the original language. The infinitesimal and infinitely large numbers of nonstandard analysis (Robinson, 1961) turn out to be elements of the sets $\R$ and $\N$ themselves rather than of extensions of them (Nelson, 1977). This is IST.
• 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 five axiomatic systems — ZFC, NBG, ZFA in Aczel's sense, NF and IST — 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 (§ 5).

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}$. In the IST column, $\mathrm{st}(x)$ reads “$x$ is standard”; an internal formula is a formula without $\mathrm{st}$, all other formulas are external; I, S, T are the schemas of idealization, standardization and transfer (§ 3). The columns $\mathrm{Th}(M_1)$ and $\mathrm{Th}(M_2)$ are analysed in § 5.

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. In IST the restriction is of the same kind as in NF, namely by the form of the formula: the language is extended by the predicate $\mathrm{st}$, and the separation and replacement schemas admit only formulas without $\mathrm{st}$; the range of separation is, as in ZFC, an already given set. $\mathrm{Th}(M_1)$ and $\mathrm{Th}(M_2)$ have no syntactic prohibitions: missing sets are simply absent from the structure.

By transfer, every set uniquely defined by an internal formula with standard parameters is standard: such are $\varnothing$, $\N$, $\R$, $\pi$ and every explicitly given natural number. By idealization applied to the formula $x\in A\wedge x\ne y$, every infinite set $A$ contains a nonstandard element. In particular, $\N$ contains a nonstandard number $\nu$; it exceeds all standard natural numbers, and $1/\nu$ is a positive real number smaller than all standard positive reals. A set is standard and finite if and only if all its elements are standard. Idealization for the formula “$x$ is finite and $y\in x$” yields a finite set $F$ having all standard sets among its elements.

Finiteness is understood here in the internal sense: $F$ is equinumerous with a segment $\{0,\dots,N-1\}$ for some $N\in\N$. The number $N$ is nonstandard, since $F$ contains all standard natural numbers. The simplest example of the same kind is the segment $\{0,1,\dots,\nu\}$ with $\nu$ nonstandard: it is finite, has $\nu+1$ elements and contains all standard natural numbers. The set $F$ is nonstandard and contains nonstandard elements along with the standard ones; the collection of standard sets itself is not a set (§ 4).

IST is a conservative extension of ZFC: an internal sentence is provable in IST if and only if it is provable in ZFC (Nelson, 1977). Nelson's reduction algorithm converts an external formula with bounded quantifiers and standard parameters into an internal formula equivalent to it in IST; the algorithm does not extend to arbitrary formulas: there is a sentence of the language of IST that is not equivalent in IST to any internal sentence (Kanovei, 1993). The restrictions of NF and IST are compared in § 4.

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 IST the universe fails to be a set for the same reason as in ZFC. The standard sets do not form a set either, although all of them belong to some finite set: a collection may fail to be a set for reasons other than size (§ 4). 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.

In IST foundation is retained as an internal axiom of ZFC. The collection of nonstandard natural numbers is nonempty and has no least element, but it is not a set, so the well-ordering of $\N$ is not violated.

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; its general form for an arbitrary binary predicate is given in § 6. 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.
• IST retains separation for internal formulas, and Russell's argument goes through exactly as in ZFC. Excluding external formulas from the separation schema removes a different contradiction: the set $\{n\in\N:\mathrm{st}(n)\}$ would contain $0$, would be closed under the passage from $n$ to $n+1$, and would differ from $\N$.

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.

In IST Cantor's theorem is retained as an internal statement, provable already in ZFC: no set is a bijection between $X$ and $\mathcal P(X)$. This difference in cardinality is not reflected in the collections of standard elements. By idealization, all standard elements of $\mathcal P(X)$, i.e. all standard subsets of $X$, lie in some finite set $G\subseteq\mathcal P(X)$. If $X$ is infinite, the finite set $G$ maps injectively into $X$. Hence there is an injection into $X$ defined on all standard subsets of $X$, although there is no injection $\mathcal P(X)\to X$. No contradiction arises: the standard subsets of $X$ do not form a set, and $G$ is a proper part of $\mathcal P(X)$.

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, NF and IST are impredicative in the same sense. In NF the quantifiers of a stratified formula range over $V$, and $V$ is a set; in IST standardization applies to formulas with quantifiers over the whole universe, external formulas included.

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

In IST the ordinals are defined after von Neumann and have the same internal properties as in ZFC; $\omega$ and every larger ordinal contain nonstandard elements. Induction on $\N$ is provable for internal formulas. For an arbitrary formula $\Phi$ one has external induction, whose conclusion concerns standard numbers only:

It follows from ordinary induction for the set ${}^{\mathrm s}\{n\in\N:\Phi(n)\}$.

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

IST contains ZFC together with the axiom of choice. Without choice the schemas I, S and T are not conservative over ZF: if $\nu\in\N$ is nonstandard, then ${}^{\mathrm s}\{A\in\mathcal P(\N):\nu\in A\}$ is a nonprincipal ultrafilter on $\N$, and the existence of such an ultrafilter is not provable in ZF. The theory SPOT, with weakened schemas, is conservative over ZF and suffices for analysis with infinitesimals (Hrbacek and Katz, 2021).

Basic axioms

NF and IST differ from the other infinite systems in the separation schema. In NF only a subset defined by a stratifiable condition can be separated from a set $A$; 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. In IST a subset is separated only by an internal condition; for an external condition $\Phi$ and a standard set $A$, standardization yields the standard set ${}^{\mathrm s}\{x\in A:\Phi(x)\}$, which has the same standard elements as the collection $\{x\in A:\Phi(x)\}$. The axioms of IST add no new sets to those of ZFC: every internal existence statement provable in IST is provable in ZFC. The basic axioms in $M_1$ and $M_2$ are checked in § 5.

Interpretability in ZF

A theory $U$ is interpretable in a theory $T$ if the language of $T$ provides a formula $\delta(x)$ defining the domain of the interpretation and formulas translating the non-logical symbols of $U$ (for NBG also a domain for classes, for IST a formula for $\mathrm{st}$) such that the translations of all axioms of $U$ are provable in $T$. An interpretation yields a finitary proof of the implication $\mathrm{Con}(T)\to\mathrm{Con}(U)$. ZFC is interpreted in ZF by the constructible universe $L$ (Gödel, 1938): relativization to $L$ turns the axioms of ZFC into theorems of ZF. Hence every theory interpretable in ZFC is interpretable in ZF.

• ZFA. The domain of the interpretation consists of the accessible pointed graphs, equality is translated by bisimulation, and membership $a\in^*b$ by the condition “the graph $a$ is bisimilar to the subgraph of $b$ generated by one of the children of the point” (Forti and Honsell, 1983; Aczel, 1988). In the other direction, ZFC is interpreted in ZFA by the class $\mathrm{WF}$.
• NBG is not interpretable in ZF. NBG is finitely axiomatizable, so an interpretation of it would use only a finite subtheory $T_0\subset\mathrm{ZF}$. By the reflection principle ZF proves the consistency of each of its finite subtheories and would therefore prove $\mathrm{Con}(\mathrm{NBG})$; then NBG, which contains ZF, would prove its own consistency, contradicting Gödel's second theorem. The conservativity of NBG over ZFC is established differently — by expanding a model of ZFC with its definable classes (and, in the presence of global choice, by forcing); this yields no interpretation, since quantification over definable classes is not expressible by a single formula of the language of ZF. The only obstacle is the unprovability of $\mathrm{Con}(\mathrm{NBG})$ in ZF, and strengthening ZF removes it. Let SI be the statement that a strongly inaccessible cardinal exists. In ZF + SI the least such cardinal $\kappa$ is definable; sets are interpreted by the elements of $V_\kappa$, classes by the elements of $V_{\kappa+1}=\mathcal P(V_\kappa)$, and one obtains an interpretation not only of NBG but of MK. For NBG with global choice the same construction is carried out inside $L$. A weaker assumption also suffices: ZF + $\mathrm{Con}(\mathrm{ZF})$ proves $\mathrm{Con}(\mathrm{NBG})$, so NBG is interpretable in ZF + $\mathrm{Con}(\mathrm{ZF})$ by the arithmetized completeness theorem.
• NF. The model of TTT in the proof of Holmes and Wilshaw is constructed within ZFC, so ZFC proves $\mathrm{Con}(\mathrm{NF})$. This statement is arithmetical and hence provable already in ZF, and a theory whose consistency is provable in ZF is interpretable in ZF by the arithmetized completeness theorem. There is no converse interpretation: together with $\mathrm{ZF}\vdash\mathrm{Con}(\mathrm{NF})$ it would give $\mathrm{ZF}\vdash\mathrm{Con}(\mathrm{ZF})$.
• IST. For every finite set of axioms of IST a model is constructed in ZFC: by the reflection principle one takes a $V_\alpha$ satisfying the required finite fragment of ZFC, and an ultralimit of it in which $\mathrm{st}$ picks out the image of $V_\alpha$ (Nelson, 1977). Thus ZFC proves the consistency of every finite subtheory of IST, and by Orey's compactness theorem (1961) IST is interpretable in ZFC. There is, however, no uniform construction extending the universe of ZFC to a universe of IST: the class of standard sets of a model of IST is not an arbitrary model of ZFC (Kanovei and Reeken, 1997).
• $\mathrm{Th}(M_1)$ and $\mathrm{Th}(M_2)$ are interpreted by finite definable structures: for $M_1$ the domain is $\{\varnothing\}$ and $x\in^*y$ always holds; for $M_2$ the domain is $\{\varnothing,\{\varnothing\}\}$ and $x\in^*y$ means $x=y=\{\varnothing\}$.

4. Restriction by the form of the formula: NF and IST

In ZFC and ZFA every part of a set that is defined by a formula of the language is a set: a definable collection can fail to be a set only because of its size. In NF and IST the admissibility of comprehension depends on the syntactic form of the formula — stratifiability in NF, absence of the predicate $\mathrm{st}$ in IST — and a definable part of a set may fail to be a set. In the terminology of Vopěnka and Hájek (1972) such a collection is a proper semiset.

Semisets and induction

In NF the set $\N$ is defined as the intersection of all inductive sets, so induction on a condition $\varphi(n)$ requires the existence of the set $\{n\in\N:\varphi(n)\}$ and is secured only for stratifiable $\varphi$. In IST the reason is the same: induction follows from separation, and separation is restricted to internal formulas. The predicate $\mathrm{st}$ refutes unrestricted induction. By transfer, $0$ is standard and the standardness of $n$ implies that of $n+1$, while by idealization $\N$ contains nonstandard numbers. Hence the collection $\{n\in\N:\mathrm{st}(n)\}$ is not a set. Neither is the collection of all standard sets: otherwise its intersection with $\N$ would be a set.

Well-foundedness inside the theory and in the metatheory

In both theories $\N$ and the ordinals are well-ordered in the sense of the theory itself: every nonempty set has a least element. The descending chains $\Theta>T(\Theta)>T^2(\Theta)>\dots$ in NF and $\nu>\nu-1>\nu-2>\dots$ in IST are given by formulas outside the comprehension schema — an unstratifiable one in NF, an external one in IST — and do not form sets. From the standpoint of the metatheory both chains are infinite. Hence in every model of NF the ordering of the ordinals is not well-founded, and in every model of IST already the ordering of the natural numbers is not: the natural numbers of a model of IST are nonstandard in the model-theoretic sense. Nonstandard models of Peano arithmetic are discussed in “On Mathematical Induction”.

Sets on which the restriction is lifted

In NF a set $A$ is called strongly cantorian if the map $a\mapsto\{a\}$ on $A$ is a set. The type of a variable ranging over such a set can be shifted, and separation from $A$ goes through for conditions that fail to be stratifiable only because of that variable. For instance, for a strongly cantorian $A$ and $\iota_A=\{\langle a,\{a\}\rangle:a\in A\}$, the condition $x\in x$ for $x\in A$ is equivalent to the stratifiable condition $\exists s\,(\langle x,s\rangle\in\iota_A\wedge\forall u\in s\,(u\in x))$, so that $\{x\in A:x\notin x\}$ is a set.

In IST the same role is played by the standard finite sets. If $A$ is standard and finite, then all its elements are standard, and for every formula $\Phi$ the collection $\{x\in A:\Phi(x)\}$ coincides with the set $A\cap{}^{\mathrm s}\{x\in A:\Phi(x)\}$.

The external structure of a nonstandard model

A model of NFU is obtained from a model $M$ of set theory with an automorphism $j$ that moves some ordinal (Jensen, 1969; Boffa, 1988): the domain is an initial segment of the cumulative hierarchy of $M$, and the membership relation of the new model is defined from $\in^M$ and $j$. Since $j$ is an automorphism, a stratifiable formula of the new model can be rewritten as a formula of the language of $M$ without $j$, and comprehension for it follows from separation in $M$. In an unstratifiable formula $j$ remains, and the automorphism $j$ is not definable in $M$, so separation does not apply to such a formula.

The proof of the conservativity of IST (Nelson, 1977) constructs an elementary extension — an ultralimit — of a fragment of the universe of ZFC in which the predicate $\mathrm{st}$ is interpreted by the image of the original structure; this image is not definable in the extension. In both cases the comprehension schema covers the formulas that do not depend on the external structure of the nonstandard model — the automorphism in NFU, the elementary submodel in IST — and reduces to separation in that model. The models of NF itself in the proof of Holmes and Wilshaw are constructed differently.

Differences

Stratifiability is a property of the formula as a whole: a coherent assignment of types to all variables is required. Internality is the absence of a single symbol from the formula. In NF stratification is the only restriction on comprehension, and the theory is incompatible with ZFC. In IST Russell's paradox is blocked, as in ZFC, by separation from a given set; the exclusion of external formulas reconciles separation with idealization, and the internal theorems remain those of ZFC. The standardization schema, which assigns a standard set to an external condition, has no analogue in NF.

A restriction by the form of the formula is present in NBG as well: class comprehension, and with it separation and induction, are secured only for formulas without class quantifiers. Induction on $\N$ for formulas with such quantifiers is not provable in NBG but is provable in MK; the proof of the consistency of ZFC in MK rests on this (see “Predicativity”).

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

6. The impossibility of full homogeneity

The need to restrict comprehension has nothing to do with the meaning of the membership relation: it follows from predicate logic and concerns every binary predicate.

The interpretation of the predicate $P$ plays no role in the derivation. For $P(x,y)\equiv x\in y$ one obtains Russell's paradox; for $P(x,y)\equiv x\in f(y)$ with a map $f\colon A\to\mathcal P(A)$, the diagonal proof of Cantor's theorem. The derivation goes through for equality as well: for $P(x,y)\equiv x=y$ and $\varphi(x)\equiv x\ne x$ one obtains $y=y\leftrightarrow y\ne y$. Hence comprehension for any binary predicate must be restricted, and the kind of restriction is determined by which element of the schema is changed.

Three elements of the schema take part in the derivation of the contradiction. The quantifiers $\exists y$ and $\forall x$ range over the same domain, which makes the substitution $x:=y$ possible. The formula $\varphi$ is arbitrary and may, in particular, be $\neg P(x,x)$. The right-hand side of the equivalence is the formula $\varphi(x)$ itself, with no additional conditions. Naive set theory is the schema of full comprehension for the predicate $\in$, and it is homogeneous in all three respects: the objects are of one sort and each of them can be a member; all formulas of the language have equal standing; the range of comprehension is unrestricted. In it, comprehension for the formula $x\notin x$ yields Russell's paradox, for the formula “$x$ is an ordinal” the Burali-Forti paradox, and for the formula $x=x$ Cantor's paradox.

Every consistent system in the table changes at least one of the three elements of the schema, or gives up the comprehension schema altogether.

The systems differ in where the inhomogeneity is placed. Russell's theory of types and NBG distinguish objects: types in the former, sets and classes in the latter; in NBG the collection of all classes is in turn no longer an object. NF and IST keep a single sort of objects and distinguish formulas; NF is obtained from the theory of types by erasing the types of objects, and the distinction of types passes in it from objects to formulas. In ZFC and ZFA neither objects nor formulas are distinguished within the theory, but the collections $V$, $\mathrm{On}$ and $\{x:x\notin x\}$ exist only in the metalanguage, as abbreviations of formulas: the distinction between set and class is moved outside the theory.

In $M_1$ and $M_2$ there are no sorts of objects, no distinguished formulas and no restriction on the range of comprehension, but there is no comprehension schema either: $M_1$ lacks the empty set, $M_2$ lacks pairs and power sets, and neither the natural numbers nor the ordinals are represented in these structures. Homogeneity is attained in them at the cost of expressive power.

The columns of the table thus correspond to ways of placing one and the same inhomogeneity: between sorts of objects, between kinds of formulas, between the theory and the metalanguage, or between the sets that exist and those that are absent. It cannot be eliminated, for purely logical reasons that do not depend on the concept of set.

7. Positions: Zermelo, Hilbert, von Neumann, Quine, Aczel, Nelson, Grothendieck, Grzegorczyk, 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); nonstandard analysis to Robinson (1961), the notion of semiset to Vopěnka and Hájek (1972); the analysis of the iterative conception as a justification of the ZFC axioms to Boolos (1971).

8. Beyond the table

• HF and $\mathrm{ZF}_{\mathrm{fin}}$. The hereditarily finite sets form $V_\omega$, a model of the theory $\mathrm{ZF}_{\mathrm{fin}}$ in which the axiom of infinity is replaced by its negation. Ackermann's coding (1937) — $n\in^*m$ if the $n$-th binary digit of $m$ is $1$ — interprets $\mathrm{ZF}_{\mathrm{fin}}$ in Peano arithmetic; with the added axiom “every set is contained in a transitive set” the two theories are bi-interpretable (Kaye and Wong, 2007). The passage from naive comprehension to the hereditarily finite sets is treated in the summary of chapter B2, “The Foundations of Mathematics”.
• TC. The theory of concatenation: the objects are strings and the only operation is juxtaposition $x^\frown y$ (Tarski, 1935; Quine, 1946). Grzegorczyk's axioms (2005): associativity, the existence of a common refinement whenever $x^\frown y=u^\frown v$, and two distinct irreducible strings. The theory has neither sets nor numbers, yet it is essentially undecidable (Grzegorczyk and Zdanowski, 2008) and mutually interpretable with Robinson arithmetic Q, and through it with the set theory that postulates only the empty set and the adjunction of an element, $x\cup\{y\}$.
• 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.
• TG. Tarski–Grothendieck set theory: ZFC with the axiom of universes — every set belongs to a Grothendieck universe, i.e. to a set $V_\kappa$ with $\kappa$ strongly inaccessible. The proper classes of one universe are sets of the next.
• 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).
• BST and HST. Nonstandard set theories studied by Kanovei and Reeken (2004). BST is a variant of IST with the boundedness axiom (every set belongs to a standard set) and a correspondingly bounded idealization; in BST every formula is equivalent to a formula of the form $\exists^{\mathrm{st}}a\,\forall^{\mathrm{st}}b\,\varphi$ with $\varphi$ internal. The theory HST also has external sets as objects.
• AST. Vopěnka's alternative set theory (1979): all sets are finite in the sense of the theory, and infinity is represented by proper semisets — parts of sets that are not sets.
• 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.

9. References

Textbooks and monographs by system

• Comparison of systems. A. A. Fraenkel, Y. Bar-Hillel, A. Lévy, Foundations of Set Theory, 2nd ed., North-Holland, Amsterdam, 1973; W. V. Quine, Set Theory and Its Logic (1963).
• ZFC. T. Jech, Set Theory, 3rd millennium ed., Springer, Berlin, 2003; K. Kunen, Set Theory: An Introduction to Independence Proofs, North-Holland, Amsterdam, 1980; P. J. Cohen, Set Theory and the Continuum Hypothesis, Benjamin, New York, 1966.
• NBG and MK. K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Princeton University Press, Princeton, 1940; E. Mendelson, Introduction to Mathematical Logic, Van Nostrand, Princeton, 1964 (ch. 4, NBG); J. L. Kelley, General Topology, Van Nostrand, New York, 1955 (appendix, MK).
• ZFA. P. Aczel, Non-Well-Founded Sets (1988); J. Barwise, L. Moss, Vicious Circles, CSLI, Stanford, 1996.
• NF and NFU. J. B. Rosser, Logic for Mathematicians, McGraw-Hill, New York, 1953; T. E. Forster, Set Theory with a Universal Set, 2nd ed., Clarendon Press, Oxford, 1995; M. R. Holmes, Elementary Set Theory with a Universal Set, Academia-Bruylant, Louvain-la-Neuve, 1998.
• IST and nonstandard set theories. E. Nelson, Internal set theory (1977); A. Robert, Nonstandard Analysis, Wiley, New York, 1988; V. Kanovei, M. Reeken, Nonstandard Analysis, Axiomatically (2004); E. I. Gordon, A. G. Kusraev, S. S. Kutateladze, Infinitesimal Analysis, Kluwer, Dordrecht, 2002.
• KP, CZF, AST. J. Barwise, Admissible Sets and Structures, Springer, Berlin, 1975; P. Aczel, M. Rathjen, Notes on Constructive Set Theory, Institut Mittag-Leffler, Report No. 40, 2001; P. Vopěnka, Mathematics in the Alternative Set Theory (1979).
• Interpretability and weak theories. P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic, Springer, Berlin, 1993.

Papers and primary sources

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. W. Ackermann, Die Widerspruchsfreiheit der allgemeinen Mengenlehre, Math. Ann. 114 (1937), 305–315.
8. A. Tarski, Über unerreichbare Kardinalzahlen, Fund. Math. 30 (1938), 68–89.
9. W. V. Quine, Concatenation as a basis for arithmetic, J. Symbolic Logic 11 (1946), 105–114.
10. J. B. Rosser, H. Wang, Non-standard models for formal logics, J. Symbolic Logic 15 (1950), 113–129.
11. E. Specker, The axiom of choice in Quine's New Foundations for mathematical logic, Proc. Nat. Acad. Sci. USA 39 (1953), 972–975.
12. S. Orey, Relative interpretations, Z. Math. Logik Grundlagen Math. 7 (1961), 146–153.
13. A. Robinson, Non-standard analysis, Indag. Math. 23 (1961), 432–440.
14. J. F. Thomson, On some paradoxes, in: R. J. Butler (ed.), Analytical Philosophy, Barnes & Noble, New York, 1962, 104–119.
15. W. V. Quine, Set Theory and Its Logic, Harvard University Press, Cambridge, MA, 1963.
16. S. Feferman, Systems of predicative analysis, J. Symbolic Logic 29 (1964), 1–30.
17. S. Orey, New Foundations and the axiom of counting, Duke Math. J. 31 (1964), 655–660.
18. R. B. Jensen, On the consistency of a slight (?) modification of Quine's New Foundations, Synthese 19 (1969), 250–263.
19. G. Boolos, The iterative conception of set, J. Philos. 68 (1971), 215–231.
20. U. Felgner, Comparison of the axioms of local and universal choice, Fund. Math. 71 (1971), 43–62.
21. M. Artin, A. Grothendieck, J.-L. Verdier, Théorie des topos et cohomologie étale des schémas (SGA 4), t. 1, Lecture Notes in Math. 269, Springer, Berlin, 1972.
22. P. Vopěnka, P. Hájek, The Theory of Semisets, North-Holland, Amsterdam, 1972.
23. E. Nelson, Internal set theory: a new approach to nonstandard analysis, Bull. Amer. Math. Soc. 83 (1977), 1165–1198.
24. K. Hrbáček, Axiomatic foundations for nonstandard analysis, Fund. Math. 98 (1978), 1–19.
25. P. Vopěnka, Mathematics in the Alternative Set Theory, Teubner, Leipzig, 1979.
26. M. Forti, F. Honsell, Set theory with free construction principles, Ann. Sc. Norm. Super. Pisa Cl. Sci. (4) 10 (1983), 493–522.
27. E. Nelson, Predicative Arithmetic, Mathematical Notes 32, Princeton University Press, Princeton, 1986.
28. P. Aczel, Non-Well-Founded Sets, CSLI Lecture Notes 14, CSLI, Stanford, 1988.
29. 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.
30. M. Boffa, ZFJ and the consistency problem for NF, Jahrb. Kurt-Gödel-Ges. (1988), 102–106.
31. V. G. Kanovei, Undecidable hypotheses in Edward Nelson's internal set theory, Russian Math. Surveys 46:6 (1991), 1–54.
32. V. Kanovei, IST is more than an algorithm to prove ZFC theorems, arXiv:math/9310213 (1993).
33. V. Kanovei, M. Reeken, What internal set theory knows about standard sets, arXiv:math/9711205 (1997).
34. V. Kanovei, M. Reeken, Nonstandard Analysis, Axiomatically, Springer, Berlin, 2004.
35. A. Grzegorczyk, Undecidability without arithmetization, Studia Logica 79 (2005), 163–230.
36. R. Kaye, T. L. Wong, On interpretations of arithmetic and set theory, Notre Dame J. Formal Logic 48 (2007), 497–510.
37. K. Hrbacek, M. G. Katz, Infinitesimal analysis without the Axiom of Choice, Ann. Pure Appl. Logic 172 (2021), no. 6, 102959.
38. M. R. Holmes, S. Wilshaw, NF is consistent, arXiv:1503.01406.