View source for New Foundations

{{Short description|Axiomatic set theory devised by W.V.O. Quine}}
In [[mathematical logic]], '''New Foundations''' ('''NF''') is a [[non-well-founded set theory|non-well-founded]], [[Axiom schema#Finite axiomatization|finitely axiomatizable]] [[Set theory#Formalized set theory|set theory]] conceived by [[Willard Van Orman Quine]] as a simplification of the [[Type theory|theory of types]] of ''[[Principia Mathematica]]''.<ref>{{Cite book |last1=Fraenkel |first1=Abraham Adolf |title=Foundations of set theory |last2=Bar-Hillel |first2=Yehoshua |last3=Lévy |first3=Azriel |date=1973 |publisher=Noord-Hollandsche U.M |isbn=978-0-7204-2270-2 |edition=2d rev. |series=Studies in logic and the foundations of mathematics |location=Amsterdam |page=161|quote=One of the most interesting attempts in this direction was made by Quine}}</ref>

== Definition ==

The [[well-formed formulas]] of NF are the standard formulas of [[propositional calculus]] with two primitive predicates [[Equality (mathematics)#In logic|equality]] (<math>=</math>) and [[Set (mathematics)#Membership|membership]] (<math>\in</math>).  NF can be presented with only two axiom schemata:
* [[Extensionality]]: Two objects with the same elements are the same object; formally, given any set ''A'' and any set ''B'', if for every set ''X'', ''X'' is a member of ''A'' [[if and only if]] ''X'' is a member of ''B'', then ''A'' is [[equal (math)|equal]] to ''B''.
* A restricted [[axiom schema of comprehension]]: <math>\{x \mid \phi \}</math> exists for each [[stratified formula]] <math>\phi</math>.

A formula <math>\phi</math> is said to be ''stratified'' if there exists a [[function (mathematics)|function]] ''f'' from pieces of <math>\phi</math>'s syntax to the natural numbers, such that for any atomic subformula <math>x \in y</math> of <math>\phi</math> we have ''f''(''y'') = ''f''(''x'') + 1, while for any atomic subformula <math>x=y</math> of <math>\phi</math>, we have ''f''(''x'') = ''f''(''y'').

===Finite axiomatization===

NF can be [[Axiom schema#Finite axiomatization|finitely axiomatized]].{{sfn|Hailperin|1944}} One advantage of such a finite axiomatization is that it eliminates the notion of [[stratification (mathematics)|stratification]]. The axioms in a finite axiomatization correspond to natural basic constructions, whereas stratified comprehension is powerful but not necessarily intuitive. In his introductory book, Holmes opted to take the finite axiomatization as basic, and prove stratified comprehension as a theorem.{{sfn|Holmes|1998|loc=chpt. 8}} The precise set of axioms can vary, but includes most of the following, with the others provable as theorems:{{sfn|Holmes|1998}}{{sfn|Hailperin|1944}}
<!-- both -->
* Extensionality: If <math>A</math> and <math>B</math> are sets, and for each object <math>x</math>, <math>x</math> is an element of <math>A</math> if and only if <math>x</math> is an element of <math>B</math>, then <math>A = B</math>.{{sfn|Holmes|1998|p=16}} This can also be viewed as defining the equality symbol.{{sfn|Hailperin|1944|loc=Definition 1.02 and Axiom PId}}<ref>For example [[W. V. O. Quine]], ''Mathematical Logic'' (1981) uses "three primitive notational devices: membership, joint denial, and quantification", then defines = in this fashion (pp.134–136)</ref>
* Singleton: For every object <math>x</math>, the set <math>\iota(x) = \{x\} = \{y | y = x\}</math> exists, and is called the singleton of <math>x</math>.{{sfn|Holmes|1998|p=25}}{{sfn|Fenton|2015|loc=ax-sn}}
* Cartesian Product: For any sets <math>A</math>, <math>B</math>, the set <math>A \times B = \{(a, b) | a \in A \text{ and } b \in B\}</math>, called the Cartesian product of <math>A</math> and <math>B</math>, exists.{{sfn|Holmes|1998|p=27}} This can be restricted to the existence of one of the cross products <math>A \times V</math> or <math>V \times B</math>.{{sfn|Hailperin|1944|p=10|loc=Axiom P5}}{{sfn|Fenton|2015|loc=ax-xp}}
* Converse: For each relation <math>R</math>, the set <math>R^{-1} = \{(x, y) | (y,x) \in R\}</math> exists; observe that <math>x R^{-1} y</math> exactly if <math>y R x</math>.{{sfn|Holmes|1998|p=31}}{{sfn|Hailperin|1944|p=10|loc=Axiom P7}}{{sfn|Fenton|2015|loc=ax-cnv}}
* Singleton Image: For any relation <math>R</math>, the set <math>R\iota = \{(\{x\}, \{y\}) | (x,y) \in R\}</math>, called the singleton image of <math>R</math>, exists.{{sfn|Holmes|1998|p=32}}{{sfn|Hailperin|1944|p=10|loc=Axiom P2}}{{sfn|Fenton|2015|loc=ax-si}}
* Domain: If <math>R</math> is a relation, the set <math>\text{dom}(R) = \{x | \exists y. (x,y) \in R\}</math>, called the domain of <math>R</math>, exists.{{sfn|Holmes|1998|p=31}} This can be defined using the operation of type lowering.{{sfn|Hailperin|1944|p=10}}
* Inclusion: The set <math>[\subseteq] = \{(x, y) | x \subseteq y\}</math> exists.{{sfn|Holmes|1998|p=44}} Equivalently, we may consider the set <math>[\in] = [\subseteq] \cap (1 \times V) = \{(\{x\}, y) | x \in y\}</math>.{{sfn|Hailperin|1944|p=10|loc=Axiom P9}}{{sfn|Fenton|2015|loc=ax-sset}}
* Complement: For each set <math>A</math>, the set <math>A^c = \{x | x \notin A\}</math>, called the complement of <math>A</math>, exists.{{sfn|Holmes|1998|p=19}}
* (Boolean) Union: If <math>A</math> and <math>B</math> are sets, the set <math>A \cup B = \{x | x \in A \text{ or } x \in B \text{ or both}\}</math>, called the (Boolean) union of <math>A</math> and <math>B</math>, exists.{{sfn|Holmes|1998|p=20}}
* Universal Set: <math>V = \{x | x = x\}</math> exists. It is straightforward that for any set <math>x</math>, <math>x \cup x^c = V</math>.{{sfn|Holmes|1998|p=19}}
* Ordered Pair: For each <math>a</math>, <math>b</math>, the ordered pair of <math>a</math> and <math>b</math>, <math>(a, b)</math>, exists; <math>(a, b) = (c, d)</math> exactly if <math>a = c</math> and <math>b = d</math>. This and larger tuples can be a definition rather than an axiom if an ordered pair construction is used.{{sfn|Holmes|1998|pp=26-27}}
* Projections: The sets <math>\pi_1 = \{((x, y), x) | x, y \in V \}</math> and <math>\pi_2 = \{((x, y), y) | x, y \in V \}</math> exist (these are the relations which an ordered pair has to its first and second terms, which are technically referred to as its projections).{{sfn|Holmes|1998|p=30}}
* Diagonal: The set <math>[=] = \{(x, x) | x \in V \}</math> exists, called the equality relation.{{sfn|Holmes|1998|p=30}}
* Set Union: If <math>A</math> is a set all of whose elements are sets, the set <math>\bigcup [A] = \{x | \text{for some } B, x \in B \text{ and } B \in A\}</math>, called the (set) union of <math>A</math>, exists.{{sfn|Holmes|1998|p=24}}
* Relative Product: If <math>R</math>, <math>S</math> are relations, the set <math>(R|S) = \{(x, y) | \text{for some } z, x R z \text{ and } z S y\}</math>, called the relative product of <math>R</math> and <math>S</math>, exists.{{sfn|Holmes|1998|p=31}}
* Anti-intersection: <math>x|y = \{z : \neg(z \in x \land z \in y) \}</math> exists. This is equivalent to complement and union together, with <math>x^c = x|x</math> and <math>x \cup y =x^c|y^c</math>.{{sfn|Fenton|2015|loc=ax-nin}}
* Cardinal one: The set <math>1</math> of all singletons, <math>\{ x | \exists y : (\forall w : w \in x \leftrightarrow w = y) \}</math>, exists.{{sfn|Hailperin|1944|p=10|loc=Axiom P8}}{{sfn|Fenton|2015|loc=ax-1c}}
* Tuple Insertions: For a relation <math>R</math>, the sets <math>I_2(R) = \{ (z, w, t) : (z, t) \in R \}</math> and <math>I_3(R) = \{ (z, w, t) : (z, w) \in R \}</math> exist.{{sfn|Hailperin|1944|p=10|loc=Axioms P3,P4}}{{sfn|Fenton|2015|loc=ax-ins2,ax-ins3}}
* Type lowering: For any set <math>S</math>, the set <math>\text{TL}(S) = \{ z : \forall w : (w, \{z\}) \in S \}</math> exists.{{sfn|Hailperin|1944|p=10|loc=Axiom P6}}{{sfn|Fenton|2015|loc=ax-typlower}}

=== Typed Set Theory ===
New Foundations is closely related to '''Russellian unramified typed set theory''' ('''TST'''), a streamlined version of the theory of types of ''Principia Mathematica'' with a linear hierarchy of types.  In this [[Structure (mathematical logic)#Many-sorted structures|many-sorted]] theory, each variable and set is assigned a type. It is customary to write the ''type indices'' as superscripts: <math>x^n</math> denotes a variable of type ''n''. Type 0 consists of individuals otherwise undescribed. For each (meta-) [[natural number]] ''n'', type ''n''+1 objects are sets of type ''n'' objects; objects connected by identity have equal types and sets of type ''n'' have members of type ''n''-1. The axioms of TST are extensionality, on sets of the same (positive) type, and comprehension, namely that if <math>\phi(x^n)</math>{{Hair space}}is a formula, then the set <math>\{x^n \mid \phi(x^n)\}^{n+1}\!</math> exists. In other words, given any formula <math>\phi(x^n)\!</math>, the formula <math>\exists A^{n+1} \forall x^n [ x^n \in A^{n+1} \leftrightarrow \phi(x^n) ]</math> is an axiom where <math>A^{n+1}\!</math> represents the set <math>\{x^n \mid \phi(x^n)\}^{n+1}\!</math> and is not [[Free variables and bound variables|free]] in <math>\phi(x^n)</math>. This type theory is much less complicated than the one first set out in the ''Principia Mathematica'', which included types for [[Relation (mathematics)|relations]] whose arguments were not necessarily all of the same types.

There is a correspondence between New Foundations and TST in terms of adding or erasing type annotations. In NF's comprehension schema, a formula is stratified exactly when the formula can be assigned types according to the rules of TST. This can be extended to map every NF formula to a set of corresponding TST formulas with various type index annotations. The mapping is one-to-many because TST has many similar formulas. For example, raising every type index in a TST formula by 1 results in a new, valid TST formula.

=== Tangled Type Theory ===

Tangled Type Theory (TTT) is an extension of TST where each variable is typed by an ordinal rather than a natural number. The well-formed atomic formulas are <math>x^{n} = y^{n}</math> and <math>x^{m} \in y^{n}</math> where <math>m<n</math>. The axioms of TTT are those of TST where each variable of type <math>i</math> is mapped to a variable <math>s(i)</math> where <math>s</math> is an increasing function.

TTT is considered a "weird" theory because each type is related to ''each'' lower type in the same way. For example, type 2 sets have both type 1 members and type 0 members, and extensionality axioms assert that a type 2 set is determined uniquely by ''either'' its type 1 members or its type 0 members. Whereas TST has natural models where each type <math>i + 1</math> is the power set of type <math>i</math>, in TTT each type is being interpreted as the power set of each lower type simultaneously. Regardless, a model of NF can be easily converted to a model of TTT, because in NF all the types are already one and the same. Conversely, with a more complicated argument, it can also be shown that the consistency of TTT implies the consistency of NF.<ref name="HolmesConNF" />

=== NFU and other variants ===
'''NF with [[urelement]]s''' ('''NFU''') is an important variant of NF due to Jensen<ref name="Jensen1968" /> and clarified by Holmes.{{sfn|Holmes|1998}} Urelements are objects that are not sets and do not contain any elements, but can be contained in sets. One of the simplest forms of axiomatization of NFU regards urelements as multiple, unequal empty sets, thus weakening the extensionality axiom of NF to:
* Weak extensionality: Two ''non-empty'' objects with the same elements are the same object; formally,
:<math display="block">\forall x y w. (w \in x) \to (x = y \leftrightarrow (\forall z. z \in x \leftrightarrow z \in y)))</math>
In this axiomatization, the comprehension schema is unchanged, although the set <math>\{x \mid \phi(x)\}</math> will not be unique if it is empty (i.e. if <math>\phi(x)</math> is unsatisfiable).

However, for ease of use, it is more convenient to have a unique, "canonical" empty set. This can be done by introducing a sethood predicate <math>\mathrm{set}(x)</math> to distinguish sets from atoms. The axioms are then:
* Sets: Only sets have members, i.e. <math>\forall x y. x \in y \to \mathrm{set}(y).</math>
* Extensionality: Two ''sets'' with the same elements are the same set, i.e. <math>\forall y z. (\mathrm{set}(y) \wedge \mathrm{set}(z) \wedge (\forall x. x \in y \leftrightarrow x \in z)) \to y = z.</math>
* Comprehension: The ''set'' <math>\{x \mid \phi(x) \}</math> exists for each stratified formula <math>\phi(x)</math>, i.e. <math>\exists A. \mathrm{set}(A) \wedge (\forall x. x \in A \leftrightarrow \phi(x)).</math>

NF<sub>3</sub> is the fragment of NF with full extensionality (no urelements) and those instances of comprehension which can be stratified using at most three types.  NF<sub>4</sub> is the same theory as NF.

Mathematical Logic (ML) is an extension of NF that includes proper classes as well as sets. ML was proposed by Quine and revised by Hao Wang, who proved that NF and the revised ML are equiconsistent.<ref name="WangHao1950" />

== Constructions ==

This section discusses some problematic constructions in NF. For a further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see [[implementation of mathematics in set theory]].

=== Ordered pairs ===
[[Relation (mathematics)|Relations]] and [[function (mathematics)|functions]] are defined in TST (and in NF and NFU) as sets of [[ordered pair]]s in the usual way. For purposes of stratification, it is desirable that a relation or function is merely one type higher than the type of the members of its field. This requires defining the ordered pair so that its type is the same as that of its arguments (resulting in a '''type-level''' ordered pair). The usual definition of the ordered pair, namely <math>(a, \ b)_K \; := \  \{ \{ a \}, \ \{ a, \ b \} \}</math>, results in a type two higher than the type of its arguments ''a'' and ''b''. Hence for purposes of determining stratification, a function is three types higher than the members of its field. NF and related theories usually employ [[Ordered pair#Quine–Rosser definition|Quine's set-theoretic definition]] of the ordered pair, which yields a type-level ordered pair. However, Quine's definition relies on set operations on each of the elements ''a'' and ''b'', and therefore does not directly work in NFU.

As an alternative approach, Holmes{{sfn|Holmes|1998}} takes the ordered pair ''(a, b)'' as a [[primitive notion]], as well as its left and right [[projection (mathematics)|projection]]s <math>\pi_1</math> and <math>\pi_2</math>, i.e., functions such that <math>\pi_1((a, b)) = a</math> and <math>\pi_2((a, b)) = b</math> (in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of <math>\{x \mid \phi \}</math> for any stratified formula <math>\phi</math> is considered a theorem and only proved later, so expressions like <math>\pi_1 = \{((a, b), a) \mid a, b \in V\}</math> are not considered proper definitions). Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive) usually does not matter.

=== Natural numbers and the axiom of infinity ===
The usual form of the [[axiom of infinity]] is based on the [[Set-theoretic definition of natural numbers|von Neumann construction of the natural numbers]], which is not suitable for NF, since the description of the successor operation (and many other aspects of von Neumann numerals) is necessarily unstratified. The usual form of natural numbers used in NF follows [[Set-theoretic definition of natural numbers#Frege and Russell|Frege's definition]], i.e., the natural number ''n'' is represented by the set of all sets with ''n'' elements. Under this definition, 0 is easily defined as <math>\{\varnothing\}</math>, and the successor operation can be defined in a stratified way: <math>S(A) = \{a \cup \{x\} \mid a \in A \wedge x \notin a\}.</math> Under this definition, one can write down a statement analogous to the usual form of the axiom of infinity. However, that statement would be trivially true, since the universal set <math>V</math> would be an [[Axiom of infinity|inductive set]].

Since inductive sets always exist, the set of natural numbers <math>\mathbf{N}</math> can be defined as the intersection of all inductive sets. This definition enables [[mathematical induction]] for stratified statements <math>P(n)</math>, because the set <math>\{n \in \mathbf{N} \mid P(n)\}</math> can be constructed, and when <math>P(n)</math> satisfies the conditions for mathematical induction, this set is an inductive set.

Finite sets can then be defined as sets that belong to a natural number. However, it is not trivial to prove that <math>V</math> is not a "finite set", i.e., that the size of the universe <math>|V|</math> is not a natural number. Suppose that <math>|V| = n \in \mathbf{N}</math>. Then <math>n = \{V\}</math> (it can be shown inductively that a finite set is not [[equinumerous]] with any of its proper subsets), <math>n + 1 = S(n) = \varnothing</math>, and each subsequent natural number would be <math>\varnothing</math> too, causing arithmetic to break down. To prevent this, one can introduce the '''axiom of infinity''' for NF: <math>\varnothing \notin \mathbf{N}.</math>{{sfn|Holmes|1998|loc=sec. 12.1}}

It may intuitively seem that one should be able to prove ''Infinity'' in NF(U) by constructing any "externally" infinite sequence of sets, such as <math>\varnothing, \{\varnothing\}, \{\{{\varnothing}\}\}, \ldots</math>. However, such a sequence could only be constructed through unstratified constructions (evidenced by the fact that TST itself has finite models), so such a proof could not be carried out in NF(U). In fact, ''Infinity'' is [[Independence (mathematical logic)|logically independent]] of NFU: There exists models of NFU where <math>|V|</math> is a [[Non-standard model of arithmetic|non-standard natural number]]. In such models, mathematical induction can prove statements about <math>|V|</math>, making it impossible to "distinguish" <math>|V|</math> from standard natural numbers.

However, there are some cases where ''Infinity'' can be proven (in which cases it may be referred to as the '''theorem of infinity'''):

* In NF (without [[urelement]]s), Specker<ref name="Specker1953">{{Cite journal |last=Specker |first=Ernst P. |date=1953-09-15 |title=The Axiom of Choice in Quine's New Foundations for Mathematical Logic |journal=Proceedings of the National Academy of Sciences |language=en |volume=39 |issue=9 |pages=972–975 |doi=10.1073/pnas.39.9.972 |doi-access=free |issn=0027-8424 |pmc=1063889 |pmid=16589362 |bibcode=1953PNAS...39..972S }}</ref> has shown that the [[axiom of choice]] is false. Since it can be proved through induction that every finite set has a choice function (a stratified condition), it follows that <math>V</math> is infinite.
* In NFU with axioms asserting the existence of a type-level ordered pair, <math>V</math> is equinumerous with its proper subset <math>V \times \{0\}</math>, which implies ''Infinity''.{{sfn|Holmes|2017|loc=p.91, Theorem}} Conversely, NFU + ''Infinity'' + ''Choice'' proves the existence of a type-level ordered pair. NFU + ''Infinity'' interprets NFU + "there is a type-level ordered pair" (they are not quite the same theory, but the differences are inessential).{{sfn|Holmes|2017|loc=p.91, section 2.6.1}}

Stronger axioms of infinity exist, such as that the set of natural numbers is a strongly Cantorian set, or NFUM = NFU + ''Infinity'' + ''Large Ordinals'' + ''Small Ordinals'' which is equivalent to [[Morse–Kelley set theory]] plus a predicate on proper classes which is a ''κ''-complete nonprincipal ultrafilter on the proper class ordinal ''κ''.<ref name="HolmesStrongInf" />

=== Large sets ===
NF (and NFU + ''Infinity'' + ''Choice'', described below and known consistent) allow the construction of two kinds of sets that [[ZFC]] and its proper extensions disallow because they are "too large" (some set theories admit these entities under the heading of [[proper class]]es):
* ''The [[universal set]] V''. Because <math>x=x</math> is a [[stratified formula]], the [[universal set]] ''V'' = {''x'' | ''x=x''} exists by ''Comprehension''. An immediate consequence is that all sets have [[complement (set theory)|complements]], and the entire set-theoretic universe under NF has a [[Boolean algebra (structure)|Boolean]] structure.
* ''[[cardinal number|Cardinal]] and [[ordinal number|ordinal]] numbers''. In NF (and TST), the set of all sets having ''n'' elements (the [[circular reasoning|circularity]] here is only apparent) exists. Hence [[Frege]]'s definition of the cardinal numbers works in NF and NFU: a cardinal number is an [[equivalence class]] of sets under the [[Relation (mathematics)|relation]] of [[equinumerosity]]: the sets ''A'' and ''B'' are equinumerous if there exists a [[bijection]] between them, in which case we write <math>A \sim B</math>. Likewise, an ordinal number is an [[equivalence class]] of [[well-ordering|well-ordered]] sets.

=== Cartesian closure ===
The category whose objects are the sets of NF and whose arrows are the functions between those sets is not [[cartesian closed category|Cartesian closed]]; Since NF lacks Cartesian closure, not every function [[currying|curries]] as one might intuitively expect, and NF is not a [[topos]].<ref>{{cite web |url=http://www.dpmms.cam.ac.uk/~tf/cartesian-closed.pdf |title=Why the Sets of NF do not form a Cartesian-closed Category |first=Thomas |last=Forster |date=October 14, 2007 |website=www.dpmms.cam.ac.uk}}</ref>

== Resolution of set-theoretic paradoxes ==

NF may seem to run afoul of problems similar to those in [[naive set theory]], but this is not the case. For example, the existence of the impossible [[Russell's paradox|Russell class]] <math>\{x \mid x \not\in x\}</math> is not an axiom of NF, because <math> x \not\in x </math> cannot be stratified. NF steers clear of the three well-known [[paradox]]es of [[set theory]] in drastically different ways than how those paradoxes are resolved in well-founded set theories such as ZFC. Many useful concepts that are unique to NF and its variants can be developed from the resolution of those paradoxes.

=== Russell's paradox ===
The resolution of [[Russell's paradox]] is trivial: <math>x \not\in x</math> is not a stratified formula, so the existence of <math>\{x \mid x \not\in x\}</math> is not asserted by any instance of ''Comprehension''. Quine said that he constructed NF with this paradox uppermost in mind.<ref>{{cite book |last=Quine | first=Willard Van Orman |year=1987 |url=https://www.hup.harvard.edu/catalog.php?isbn=9780674798373 |chapter=The Inception of “New Foundations” |title=Selected Logic Papers - Enlarged Edition |isbn=9780674798373 |publisher=Harvard University Press}}</ref>

=== Cantor's paradox and Cantorian sets ===
[[Cantor's paradox]] boils down to the question of whether there exists a largest [[cardinal number]], or equivalently, whether there exists a set with the largest [[cardinality]]. In NF, the [[universal set]] <math>V</math> is obviously a set with the largest cardinality. However, [[Cantor's theorem]] says (given ZFC) that the [[power set]] <math>P(A)</math> of any set <math>A</math> is larger than <math>A</math> (there can be no [[Injective function|injection]] (one-to-one map) from <math>P(A)</math> into <math>A</math>), which seems to imply a contradiction when <math>A = V</math>.

Of course there is an [[Injective function|injection]] from <math>P(V)</math> into <math>V</math> since <math>V</math> is the universal set, so it must be that Cantor's theorem (in its original form) does not hold in NF. Indeed, the proof of Cantor's theorem uses the [[diagonalization argument]] by considering the set <math>B = \{x \in A \mid x \notin f(x)\}</math>. In NF, <math>x</math> and <math>f(x)</math> should be assigned the same type, so the definition of <math>B</math> is not stratified. Indeed, if <math>f: P(V) \to V</math> is the trivial injection <math>x \mapsto x</math>, then <math>B</math> is the same (ill-defined) set in Russell's paradox.

This failure is not surprising since <math>|A| < |P(A)|</math> makes no sense in TST: the type of <math>P(A)</math> is one higher than the type of <math>A</math>. In NF, <math>|A| < |P(A)|</math> is a syntactical sentence due to the conflation of all the types, but any general proof involving ''Comprehension'' is unlikely to work.

The usual way to correct such a type problem is to replace <math>A</math> with <math>P_1(A)</math>, the set of one-element subsets of <math>A</math>. Indeed, the correctly typed version of Cantor's theorem <math>|P_1(A)| < |P(A)|</math> is a theorem in TST (thanks to the diagonalization argument), and thus also a theorem in NF. In particular, <math>|P_1(V)| < |P(V)|</math>: there are fewer one-element sets than sets (and so fewer one-element sets than general objects, if we are in NFU). The "obvious" [[bijection]] <math>x \mapsto \{x\}</math> from the universe to the one-element sets is not a set; it is not a set because its definition is unstratified. Note that in all models of NFU + ''Choice'' it is the case that <math>|P_1(V)| < |P(V)| \ll |V|</math>; ''Choice'' allows one not only to prove that there are urelements but that there are many cardinals between <math>|P(V)|</math> and <math>|V|</math>.

However, unlike in TST, <math>|A| = |P_1(A)|</math> is a syntactical sentence in NF(U), and as shown above one can talk about its truth value for specific values of <math>A</math> (e.g. when <math>A = V</math> it is false). A set <math>A</math> which satisfies the intuitively appealing <math>|A| = |P_1(A)|</math> is said to be '''Cantorian''': a Cantorian set satisfies the usual form of [[Cantor's theorem]]. A set <math>A</math> which satisfies the further condition that <math>(x \mapsto \{x\})\lceil A</math>, the [[restriction (mathematics)|restriction]] of the [[singleton (mathematics)|singleton]] map to ''A'', is a set is not only Cantorian set but '''strongly Cantorian'''.{{sfn|Holmes|1998|loc=sec. 17.5}}

=== {{Anchor|Burali-Forti paradox}}Burali-Forti paradox and the T operation ===
The ''[[Burali-Forti paradox]]'' of the largest [[ordinal number]] is resolved in the opposite way: In NF, having access to the set of ordinals does not allow one to construct a "largest ordinal number". One can construct the ordinal <math>\Omega</math> that corresponds to the natural well-ordering of all ordinals, but that does not mean that <math>\Omega</math> is larger than all those ordinals.

To formalize the Burali-Forti paradox in NF, it is necessary to first formalize the concept of ordinal numbers. In NF, ordinals are defined (in the same way as in [[naive set theory]]) as [[equivalence class]]es of [[well-ordering]]s under [[isomorphism]]. This is a stratified definition, so the set of ordinals <math>\mathrm{Ord}</math> can be defined with no problem. [[Transfinite induction]] works on stratified statements, which allows one to prove that the natural ordering of ordinals (<math>\alpha \le \beta</math> iff there exists well-orderings <math>R \in \alpha, S \in \beta</math> such that <math>S</math> is a continuation of <math>R</math>) is a well-ordering of <math>\mathrm{Ord}</math>. By definition of ordinals, this well-ordering also belongs to an ordinal <math>\Omega \in \mathrm{Ord}</math>. In naive set theory, one would go on to prove by transfinite induction that each ordinal <math>\alpha</math> is the order type of the natural order on the ordinals less than <math>\alpha</math>, which would imply an contradiction since <math>\Omega</math> by definition is the order type of ''all'' ordinals, not any proper initial segment of them.

However, the statement "<math>\alpha</math> is the order type of the natural order on the ordinals less than <math>\alpha</math>" is not stratified, so the transfinite induction argument does not work in NF. In fact, "the order type <math>\beta</math> of the natural order <math>R_\alpha</math> on the ordinals less than <math>\alpha</math>" is at least ''two'' types higher than <math>\alpha</math>: The order relation <math>R_\alpha = \{(x, y) \mid x \le y < \alpha\}</math> is one type higher than <math>\alpha</math> assuming that <math>(x, y)</math> is a [[#Ordered pairs|type-level ordered pair]], and the order type (equivalence class) <math>\beta = \{S \mid S \sim R_\alpha\}</math> is one type higher than <math>R_\alpha</math>. If <math>(x, y)</math> is the usual Kuratowski ordered pair (two types higher than <math>x</math> and <math>y</math>), then <math>\beta</math> would be ''four'' types higher than <math>\alpha</math>.

To correct such a type problem, one needs the '''T operation''', <math>T(\alpha)</math>, that "raises the type" of an ordinal <math>\alpha</math>, just like how <math>P_1(A)</math> "raises the type" of the set <math>A</math>. The T operation is defined as follows: If <math>W \in \alpha</math>, then <math>T(\alpha)</math> is the order type of the order <math>W^{\iota} = \{(\{x\},\{y\}) \mid xWy\}</math>. Now the lemma on order types may be restated in a stratified manner:
:The order type of the natural order on the ordinals <math> < \alpha</math> is <math>T^2(\alpha)</math> or <math>T^4(\alpha)</math>, depending on which ordered pair is used.
Both versions of this statement can be proven by transfinite induction; we assume the type level pair hereinafter. This means that <math>T^2(\alpha)</math> is always less than <math>\Omega</math>, the order type of ''all'' ordinals. In particular, <math>T^2(\Omega)<\Omega</math>.

Another (stratified) statement that can be proven by transfinite induction is that T is a strictly [[monotonic function|monotone]] (order-preserving) operation on the ordinals, i.e., <math>T(\alpha) < T(\beta)</math> iff <math>\alpha < \beta</math>. Hence the T operation is not a function: The collection of ordinals <math>\{\alpha \mid T(\alpha) < \alpha\}</math> cannot have a least member, and thus cannot be a set. More concretely, the monotonicity of T implies <math>\Omega > T^2(\Omega) > T^4(\Omega)\ldots</math>, a "descending sequence" in the ordinals which also cannot be a set.

One might assert that this result shows that no model of NF(U) is "[[Intended interpretation|standard]]", since the ordinals in any model of NFU are externally not well-ordered. This is a philosophical question, not a question of what can be proved within the formal theory. Note that even within NFU it can be proven that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe <math>V</math> is a model of NFU, despite <math>V</math> being a set, because the membership relation is not a set relation.

== Consistency ==

Some mathematicians had questioned the [[consistency]] of NF, partly because it is not clear why it avoids the known paradoxes. A key issue was that Specker proved NF combined with the [[Axiom of Choice]] is inconsistent. The proof is complex and involves T-operations.

However, since 2010, Holmes has claimed to have shown that NF is consistent relative to the consistency of standard set theory (ZFC). In 2024, Sky Wilshaw demonstrated the most complex part of Holmes's proof, particularly the construction of a model for Tangled Type Theory (TTT) using the [[Lean (proof assistant)|Lean proof assistant]]. Almost all conclusions regarding the independence of ZFC can be transferred to this consistency proof of NF. To be precise:  It cannot be expected that NF proves any strictly local stratified result about familiar mathematical objects which is not also a theorem of ZFC. All combinations of NF-style higher infinite and NF can be obtained by analogy from this consistency proof. However, there are still some global choice-like problems that cannot be solved by this consistency proof, such as NF+"<math>V</math> is [[Total order|linearly ordered]]", NF+[[Boolean prime ideal theorem|PIT]], and NF+[https://karagila.org/2014/on-the-partition-principle/ PP].<ref name="HolmesConNF" /> There are also certain global choice-like problems that have been proven to explicitly fail in NF, such as the existence of a non-Cantorian ordinal <math>\alpha</math> such that <math>\mathsf{NF(U)+DC}(\alpha)</math> is inconsistent.<ref>{{Cite thesis 
|  title=NF
|  last=Forster 
|  first=Thomas Edward
|  type=Ph.D. Thesis
|  publisher=University of Cambridge Repository
|  url=https://www.repository.cam.ac.uk/handle/1810/223940 
|  doi=10.17863/cam.16205 
|  date=1977-07-27
|  language=en}}</ref>

=== Models of NFU ===
Although NFU resolves the paradoxes similarly to NF, it has a much simpler consistency proof. The proof can be formalized within [[Peano Arithmetic]] (PA), a theory weaker than ZF that most mathematicians accept without question. This does not conflict with [[Gödel's second incompleteness theorem]] because NFU does not include the [[Axiom of Infinity]] and therefore PA cannot be modeled in NFU, avoiding a contradiction. PA also proves that NFU with Infinity and NFU with both Infinity and Choice  are [[equiconsistent]] with TST with Infinity and TST with both Infinity and Choice, respectively. Therefore, a stronger theory like ZFC, which proves the consistency of TST, will also prove the consistency of NFU with these additions.<ref name="Jensen1968" /> In simpler terms, NFU is generally seen as weaker than NF because, in NFU, the collection of all sets (the power set of the universe) can be smaller than the universe itself, especially when urelements are included, as required by NFU with Choice.
<!-- Where the starting point for the [[metamathematics]] of [[Zermelo–Fraenkel set theory|Zermelo-Fraenkel set theory]] is the easy-to-formalize intuition of the [[cumulative hierarchy]], the non-well-foundedness of NF and NFU makes this intuition not directly applicable. However, the intuition of forming sets at a stage from sets developed at earlier stages can be augmented to allow forming sets at a stage consisting of all possible sets but given sets formed at earlier stages, giving an analogous iterative conception of set.{{sfn|Forster|2008}}{{Specify|reason=Does this actually give a model for NFU? The cited paper only gives a model for NF_2, a significantly simpler theory.|date=July 2023}} -->

Boffa gives a fairly simple method for producing models of NFU in bulk. Using well-known techniques of [[model theory]], one can construct a nonstandard model of [[Zermelo set theory]] (nothing nearly as strong as full ZFC is needed for the basic technique) on which there is an external [[automorphism]] ''j'' (not a set of the model) which moves a [[rank (set theory)|rank]] <math>V_{\alpha}</math>{{ref label|Models of NFU|1}} of the [[cumulative hierarchy]] of sets.  We may suppose without loss of generality that <math>j(\alpha)<\alpha</math>.

The domain of the model of NFU will be the nonstandard rank <math>V_{\alpha}</math>. The basic idea is that the automorphism ''j'' codes the "power set" <math>V_{\alpha+1}</math> of our "universe" <math>V_{\alpha}</math> into its externally isomorphic copy <math>V_{j(\alpha)+1}</math> inside our "universe." The remaining objects not coding subsets of the universe are treated as [[urelement]]s. Formally, the membership relation of the model of NFU will be <math>x \in_{NFU} y \equiv_{def} j(x) \in y \wedge y \in V_{j(\alpha)+1}.</math>

It may now be proved that this actually is a model of NFU. Let <math>\phi</math> be a stratified formula in the language of NFU. Choose an assignment of types to all variables in the formula which witnesses the fact that it is stratified. Choose a natural number ''N'' greater than all types assigned to variables by this stratification. Expand the formula <math>\phi</math> into a formula <math>\phi_1</math> in the language of the nonstandard model of [[Zermelo set theory]] with [[automorphism]] ''j'' using the definition of membership in the model of NFU. Application of any power of ''j'' to both sides of an equation or membership statement preserves its [[truth value]] because ''j'' is an automorphism. Make such an application to each [[atomic formula]] in <math>\phi_1</math> in such a way that each variable ''x'' assigned type ''i'' occurs with exactly <math>N-i</math> applications of ''j''. This is possible thanks to the form of the atomic membership statements derived from NFU membership statements, and to the formula being stratified. Each quantified sentence <math>(\forall x \in V_{\alpha}.\psi(j^{N-i}(x)))</math> can be converted to the form <math>(\forall x \in j^{N-i}(V_{\alpha}).\psi(x))</math> (and similarly for [[existential quantifier]]s). Carry out this transformation everywhere and obtain a formula <math>\phi_2</math> in which ''j'' is never applied to a bound variable. Choose any free variable ''y'' in <math>\phi</math> assigned type ''i''. Apply <math>j^{i-N}</math> uniformly to the entire formula to obtain a formula <math>\phi_3</math> in which ''y'' appears without any application of ''j''. Now <math>\{y \in V_{\alpha} \mid \phi_3\}</math> exists (because ''j'' appears applied only to free variables and constants), belongs to <math>V_{\alpha+1}</math>, and contains exactly those ''y'' which satisfy the original formula
<math>\phi</math> in the model of NFU. <math>j(\{y \in V_{\alpha} \mid \phi_3\})</math> has this extension in the model of NFU (the application of ''j'' corrects for the different definition of membership in the model of NFU). This establishes that ''Stratified Comprehension'' holds in the model of NFU.

To see that weak ''Extensionality'' holds is straightforward: each nonempty element of <math>V_{j(\alpha)+1}</math> inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.

If <math>\alpha</math> is a natural number ''n'', one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course). If <math>\alpha</math> is infinite and the ''[[Axiom of Choice|Choice]]'' holds in the nonstandard model of ZFC, one obtains a model of NFU + ''Infinity'' + ''Choice''.

{{note|Models of NFU|1}}We talk about the automorphism moving the rank <math>V_{\alpha}</math> rather than the ordinal <math>\alpha</math> because we do not want to assume that every ordinal in the model is the index of a rank.

=== Self-sufficiency of mathematical foundations in NFU ===
For philosophical reasons, it is important to note that it is not necessary to work in [[ZFC]] or any related system to carry out this proof. A common argument against the use of NFU as a foundation for mathematics is that the reasons for relying on it have to do with the intuition that ZFC is correct. It is sufficient to accept TST (in fact TSTU). In outline: take the type theory TSTU (allowing urelements in each positive type) as a metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets <math>T_i</math> (all of the same type in the metatheory) with embeddings of each <math>P(T_i)</math> into <math>P_1(T_{i+1})</math> coding embeddings of the power set of <math>T_i</math> into <math>T_{i+1}</math> in a type-respecting manner). Given an embedding of <math>T_0</math> into <math>T_1</math> (identifying elements of the base "type" with subsets of the base type), embeddings may be defined from each "type" into its successor in a natural way. This can be generalized to transfinite sequences <math>T_{\alpha}</math> with care.

Note that the construction of such sequences of sets is limited by the size of the type in which they are being constructed; this prevents TSTU from proving its own consistency (TSTU + ''Infinity'' can prove the consistency of TSTU; to prove the consistency of TSTU+''Infinity'' one needs a type containing a set of cardinality <math>\beth_{\omega}</math>, which cannot be proved to exist in TSTU+''Infinity'' without stronger assumptions). Now the same results of model theory can be used to build a model of NFU and verify that it is a model of NFU in much the same way, with the <math>T_{\alpha}</math>'s being used in place of <math>V_{\alpha}</math> in the usual construction. The final move is to observe that since NFU is consistent, we can drop the use of absolute types in our metatheory, bootstrapping the metatheory from TSTU to NFU.

=== Facts about the automorphism ''j'' ===
The [[automorphism]] ''j'' of a model of this kind is closely related to certain natural operations in NFU. For example, if ''W'' is a [[well-ordering]] in the nonstandard model (we suppose here that we use [[ordered pair|Kuratowski pairs]] so that the coding of functions in the two theories will agree to some extent) which is also a well-ordering in NFU (all well-orderings of NFU are well-orderings in the nonstandard model of Zermelo set theory, but not vice versa, due to the formation of [[urelement]]s in the construction of the model), and ''W'' has type α in NFU, then ''j''(''W'') will be a well-ordering of type ''T''(α) in NFU.

In fact, ''j'' is coded by a function in the model of NFU. The function in the nonstandard model which sends the singleton of any element of <math>V_{j(\alpha)}</math> to its sole element, becomes in NFU a function which sends each singleton {''x''}, where ''x'' is any object in the universe, to ''j''(''x''). Call this function ''Endo'' and let it have the following properties: ''Endo'' is an [[Injective function|injection]] from the set of singletons into the set of sets, with the property that ''Endo''( {''x''} ) = {''Endo''( {''y''} ) | ''y''∈''x''} for each set ''x''. This function can define a type level "membership" relation on the universe, one reproducing the membership relation of the original nonstandard model.

== History ==

In 1914, [[Norbert Wiener]] showed how to code the [[ordered pair]] as a set of sets, making it possible to eliminate the relation types of ''Principia Mathematica'' in favor of the linear hierarchy of sets in TST. The usual definition of the ordered pair was first proposed by [[Kuratowski]] in 1921. [[Willard Van Orman Quine]] first proposed NF as a way to avoid the "disagreeable consequences" of TST in a 1937 article titled ''New Foundations for Mathematical Logic''; hence the name. Quine extended the theory in his book ''Mathematical Logic'', whose first edition was published in 1940. In the book, Quine introduced the system "Mathematical Logic" or "ML", an extension of NF that included [[Class (set theory)|proper classes]] as well as [[Set (mathematics)|sets]]. The first edition's set theory married NF to the [[proper class]]es of [[Von Neumann-Bernays-Godel set theory|NBG set theory]] and included an axiom schema of unrestricted comprehension for proper classes. However, [[J. Barkley Rosser]] proved that the system was subject to the Burali-Forti paradox.<ref>{{Cite journal |last=Rosser |first=Barkley |date=1942-03-24 |title=The Burali-Forti paradox |url=https://www.cambridge.org/core/product/identifier/S0022481200037026/type/journal_article |journal=Journal of Symbolic Logic |language=en |volume=7 |issue=1 |pages=1–17 |doi=10.2307/2267550 |jstor=2267550 |issn=0022-4812}}</ref> [[Hao Wang (academic)|Hao Wang]] showed how to amend Quine's axioms for ML so as to avoid this problem.<ref name="WangHao1950" /> Quine included the resulting axiomatization in the second and final edition, published in 1951.

In 1944, [[Theodore Hailperin]] showed that ''Comprehension'' is equivalent to a finite conjunction of its instances,{{sfn|Hailperin|1944}} In 1953, [[Ernst Specker]] showed that the [[axiom of choice]] is false in NF (without [[urelement]]s).<ref name="Specker1953" /> In 1969, Jensen showed that adding [[urelement]]s to NF yields a theory (NFU) that is provably consistent.<ref name="Jensen1968" /> That same year, Grishin proved NF<sub>3</sub> consistent.<ref name="Grishin1969" /> Specker additionally showed that NF is equiconsistent with TST plus the axiom scheme of "typical ambiguity". NF is also equiconsistent with TST augmented with a "type shifting automorphism", an operation (external to the theory) which raises type by one, mapping each type onto the next higher type, and preserves equality and membership relations.<ref name="Specker1966">{{Citation |last=Specker |first=Ernst |title=Typical Ambiguity |date=1966-01-01 |work=Studies in Logic and the Foundations of Mathematics |volume=44 |pages=116–124 |editor-last=Nagel |editor-first=Ernest |url=https://www.sciencedirect.com/science/article/pii/S0049237X09705762 |access-date=2025-08-17 |series=Logic, Methodology and Philosophy of Science |publisher=Elsevier |doi=10.1016/s0049-237x(09)70576-2 |isbn=978-0-8047-0096-2 |editor2-last=Suppes |editor2-first=Patrick |editor3-last=Tarski |editor3-first=Alfred}}</ref>

In 1983, Marcel Crabbé proved consistent a system he called NFI, whose axioms are unrestricted extensionality and those instances of comprehension in which no variable is assigned a type higher than that of the set asserted to exist. This is a [[impredicative|predicativity]] restriction, though NFI is not a predicative theory: it admits enough impredicativity to define the set of natural numbers (defined as the intersection of all inductive sets; note that the inductive sets quantified over are of the same type as the set of natural numbers being defined). Crabbé also discussed a subtheory of NFI, in which only parameters ([[Free variables and bound variables|free variables]]) are allowed to have the type of the set asserted to exist by an instance of comprehension. He called the result "predicative NF" (NFP); it is, of course, doubtful whether any theory with a self-membered universe is truly predicative.<ref name="Crabbé1982" /> In 1999, Holmes has shown that NFP has the same consistency strength as the predicative theory of types of ''[[Principia Mathematica]]'' without the [[axiom of reducibility]].<ref name="Holmes1999" />

The [[Metamath]] database implemented Hailperin's finite axiomatization for New Foundations.<ref>{{cite web |last1=Fenton |first1=Scott |title=New Foundations Explorer Home Page |url=https://us.metamath.org/nfeuni/mmnf.html |website=Metamath |access-date=25 April 2024|date=2015}}</ref> Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF were available both on [[arXiv]] and on the logician's home page. His proofs were based on demonstrating the equiconsistency of a "weird" variant of TST, "tangled type theory with λ-types" (TTT<sub>λ</sub>), with NF, and then showing that TTT<sub>λ</sub> is consistent relative to ZF with atoms but without choice (ZFA) by constructing a class model of ZFA which includes "tangled webs of cardinals" in ZF with atoms and choice (ZFA+C). These proofs were "difficult to read, insanely involved, and involve the sort of elaborate bookkeeping which makes it easy to introduce errors". In 2024, Sky Wilshaw formalized a version of Holmes' proof using the proof assistant [[Lean (proof assistant)|Lean]], finally resolving the question of NF's consistency.<ref name="HolmesConNF" /> Timothy Chow characterized Wilshaw's work as showing that the reluctance of peer reviewers to engage with a difficult to understand proof can be addressed with the help of proof assistants.<ref>{{cite web |last1=Chow |first1=Timothy |title=Timothy Chow on the NF consistency proof and Lean |url=https://www.logicmatters.net/2024/05/03/timothy-chow-on-the-nf-consistency-proof-and-lean/ |website=Logic Matters |date=3 May 2024 |access-date=3 May 2024}}</ref>

== Table of the consistency strength about NF-style theory ==
{| class="wikitable"
|+Table of the consistency strength about NF-style theory
![[Beth number]]
!NF-style set theory
!ZF-style set theory
!Typed-style theory
!Higher-order arithmetic
|-
|
| colspan="2" | <math>\mathsf{KF}</math>
|<math>[\Pi^\mathcal{P}_2-\mathsf{TST}]^*</math>
<math>[\Pi^\mathcal{P}_2-\mathsf{TST}+\Pi^\mathcal{P}_1-\mathsf{Amb}]^*</math><ref name="ForsterKaye1991">{{Cite journal |last1=Forster |first1=Thomas |last2=Kaye |first2=Richard |title=End-extensions preserving power set |url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/endextensions-preserving-power-set/21B8F075476519278BB8EEA0E48B04C0 |journal=The Journal of Symbolic Logic |language=en |date=March 1991 |volume=56 |issue=1 |pages=323–328 |doi=10.2307/2274922 |jstor=2274922 |issn=0022-4812}}</ref>
|
|-
|
|<math>\mathsf{NFP}</math><ref name="Crabbé1982">{{Cite journal |last=Crabbé |first=Marcel |title=On the Consistency of an Impredicative Subsystem of Quine's NF |url=https://www.jstor.org/stable/2273386 |journal=The Journal of Symbolic Logic |date=1982 |volume=47 |issue=1 |pages=131–136 |doi=10.2307/2273386 |jstor=2273386 |hdl=2078.1/57616 |issn=0022-4812}}</ref>
|
|<math>\mathsf{TSTP+Inf}</math><ref name="Holmes1995" >{{Cite journal |last=Holmes |first=M. Randall |title=The Equivalence of NF-Style Set Theories with "Tangled" Theories; The Construction of ω-Models of Predicative NF (and more) |url=https://randall-holmes.github.io/Papers/tangled.pdf |journal=The Journal of Symbolic Logic |date=1995 |volume=60 |issue=1 |doi=10.2307/2275515 |jstor=2275515 |issn=0022-4812 |access-date=2025-07-17}}</ref>
<math>\mathsf{RTT}</math><ref name="Holmes1999" >{{Cite journal |last=Holmes |first=M. Randall |title=Subsystems of Quine's ''New Foundations'' with Predicativity Restrictions |url=https://randall-holmes.github.io/Papers/euclid.ndjfl.1038949535.pdf |journal=Notre Dame Journal of Formal Logic |date=1999-04-01 |volume=40 |issue=2 |doi=10.1305/ndjfl/1038949535 |issn=0029-4527 |access-date=2025-07-15}}</ref>
|<math>\trianglerighteq\ \mathsf{I\Delta_0 + exp},\mathsf{EFA}</math>
<math>\triangleleft\ \mathsf{PA}</math>
|-
|
|<math>\mathsf{NFU}</math><ref name="Jensen1968">{{Cite journal |last=Jensen |first=Ronald Björn |title=On the Consistency of a Slight (?) Modification of Quine's "New Foundations" |url=https://www.jstor.org/stable/20114640 |journal=Synthese |date=1968 |volume=19 |issue=1/2 |pages=250–264 |doi=10.1007/BF00568059 |jstor=20114640 |issn=0039-7857}}</ref><ref name="Boffa1988">{{Cite journal 
|title=ZFJ and the consistency problem for NF
|  author=Boffa, Maurice
|  journal=Jahrbuch der Kurt Gödel Gesellschaft
|  volume=1
|  number=102–106
|  pages=75–79 
|  year=1988}}</ref>{{ref label|NFU1|A}},<math>\mathsf{MLU}</math>
<math>\mathsf{NFU}^{-\infty}</math>
|
|<math>\mathsf{TSTU}</math><ref name="Holmes1995" />
|
<math>\mathsf{I\Delta_0 + exp},\mathsf{EFA}</math>{{Unreliable source?|certain=y|reason=Upon investigation, it was found that the proof of the theorem was developed by Robert Solovay in 2002 but was never published. However, multiple independently published papers have directly acknowledged the theorem as a fact and credited Robert Solovay with its proof.|date=August 2025}}
|- style="background: yellow"
|
|<math>\mathsf{NF}_3</math><ref name="Grishin1969">{{Cite journal 
|  title=Consistency of a fragment of Quine's NF system
|  author=Grishin, Vyacheslav Nikolaevich
|  journal=Doklady Akademii Nauk SSSR
|  volume=189
|  number=2
|  pages=241–243
|  year=1969
|  via=Russian Academy of Sciences
|  language=ru
|  url=https://www.mathnet.ru/eng/dan35008}}</ref>
|
|<math>\mathsf{TST}^\infty_3</math>
|
|- style="background: yellow"
|<math>\triangleleft\ \beth_{\omega_1}</math>{{ref label|iNF1|B}}
|<math>\mathsf{iNF}</math>
|
|<math>\mathsf{T}\mathbb{Z}\mathsf{T}</math>
|<math>\trianglerighteq\ \mathsf{I\Delta_0 + exp},\mathsf{EFA}</math>
|- 
|
|<math>\mathsf{NFUA}^{-\infty}</math><ref name="Enayat2006bounded">{{Cite journal
|title=From bounded arithmetic to second order arithmetic via automorphisms
|author=Enayat, Ali and Kalantari, Iraj and Moniri, Mojtaba
|journal=Logic in Tehran
|volume=26
|pages=87–113
|year=2006
|publisher=Association for Symbolic Logic
|doi=10.1201/9781439865873-5
|doi-broken-date=19 August 2025
|isbn=978-0-367-80710-8
}}</ref>
|<math>\mathrm{KPu}^r</math><ref name="Jäger84">G. Jäger, "[https://www.jstor.org/stable/2274140 The Strength of Admissibility Without Foundation]". Journal of Symbolic Logic vol. 49, no. 3 (1984).</ref><sup>p.&nbsp;869</sup>
|
|<math>\mathsf{PA}</math>
|-
|<math>\beth_{n<\omega}</math><ref name="HolmesStrongInf">{{Cite journal |last=Holmes |first=M. Randall |title=Strong Axioms of Infinity in NFU |url=https://randall-holmes.github.io/Papers/nfumcorrected.pdf |journal=The Journal of Symbolic Logic |date=2001 |volume=66 |issue=1 |pages=87–116 |doi=10.2307/2694912 |jstor=2694912 |issn=0022-4812 |access-date=2025-07-15}}</ref>
<math>\triangleleft\ \beth_{\omega}</math>
|<math>\mathsf{NFU+Inf}</math>,<ref name="Adlevsic2024">{{Cite journal |last1=Adlešić |first1=Tin |last2=Čačić |first2=Vedran |title=Boffa's construction and models for NFU |url=https://link.springer.com/article/10.1007/s11225-024-10155-9 |journal=Studia Logica |language=en |date=2024-12-13 |doi=10.1007/s11225-024-10155-9 |issn=1572-8730}}</ref> <math>\mathsf{MLU+Inf}</math>
|
|<math>\mathsf{TTTU+FlatOP}</math>
<math>\mathsf{TSTU+FlatOP}</math>{{sfn|Holmes|2017|loc=p.91, Theorem}}<br>
<math>\mathsf{TTTU+Inf}</math><br>
<math>\mathsf{TSTU+Inf}</math>{{sfn|Holmes|2017|loc=p.91, section 2.6.1}}
|
|-
|
|<math>\mathsf{NFI}</math><ref name="Crabbé1982" /><ref name="Holmes1999" />
<math>\mathsf{NFUB}^{-\infty}</math><ref name="Enayat2006bounded" /><br>
<math>\mathsf{NF}_3+\mathsf{Inf}</math><ref name="Pabion1980tt3">{{Cite journal
|title=TT₃ + AxInf est équivalent à l'arithmétique du second ordre
|author=Pabion, J. F.
|journal=Comptes Rendus de l'Académie des Sciences, Série A
|volume=290
|pages=1117–1118
|year=1980
|language=fr
|url=https://randall-holmes.github.io/Bibliography/pabiontranslation.pdf}}</ref>
|<math>\mathsf{KP}+\Pi_\omega^{\text{set}}-\mathsf{Separation}</math>
|<math>\mathsf{TSTI+Inf}</math><ref name="Holmes1995" />
<math>\mathsf{TST}^\infty_3+\mathsf{Inf}</math><ref name="Pabion1980tt3" /><br>
<math>\lambda 2</math><ref>{{Cite book |last=Blot |first=Valentin |chapter=A direct computational interpretation of second-order arithmetic via update recursion |date=2022-08-02 |title=Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science |chapter-url=https://inria.hal.science/hal-03698879/document |language=en |publisher=ACM |pages=1–11 |doi=10.1145/3531130.3532458 |isbn=978-1-4503-9351-5}}</ref>
|<math>\mathsf{Z}_2</math>,<math>\Pi^1_\infty - \mathsf{CA}</math>
|-
|<math>\trianglerighteq\beth_\omega</math>
<math>\triangleleft\ \beth_{\omega_1}</math><ref name="HolmesConNF">{{cite arXiv | last1=Randall Holmes | first1=M. | last2=Wilshaw | first2=Sky | title=NF is Consistent | date=2015 | class=math.LO | eprint=1503.01406 }}</ref>
|<math>\mathsf{NF}</math>, <math>\mathsf{ML}</math><ref name="WangHao1950">{{Cite journal |last=Wang |first=Hao |title=A formal system of logic |url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/formal-system-of-logic/24539A1EEEE19D43724147B2BD3ACB59 |journal=The Journal of Symbolic Logic |language=en |date=March 1950 |volume=15 |issue=1 |pages=25–32 |doi=10.2307/2268438 |jstor=2268438 |issn=0022-4812 |access-date=2025-07-17}}</ref><br>
<math>\mathsf{KF}+\exists</math> [[Universal set]]<br>
<math>\mathsf{NFI}</math> + [[Axiom of union]], <math>\mathsf{NFP}</math> + [[Axiom of union]]<br>
<math>\mathsf{NF}_4</math>, <math>\mathsf{NF}_3+</math>(there exists the set <math>\{\{\{x\}, y\}/x\in y\}</math>)<ref>{{Cite journal 
|  title=The method of stratification in set theory
|  author=Grishin, Vyacheslav Nikolaevich
|  journal=Russian, Ph. D. Thesis, Moscow University
|  volume=3
|  year=1972
|  via=Russian Academy of Sciences
|  language=ru}}</ref>
|<math>\mathsf{MACQ}</math><ref name="Holmes1995" />
<math>\triangleleft\ \mathsf{MAC+}</math>(a tangled web of cardinals)<ref>{{Cite arXiv |title=NF is Consistent |first1=M. Randall|last1=Holmes|first2=Sky|last2=Wilshaw |date=2015 |eprint=1503.01406v22 |class=math.LO }}</ref>
|<math>\mathsf{TTT}</math>
<math>\mathsf{TST+Amb}</math><ref name="Specker1966" /><br>
<math>\trianglelefteq\ \mathsf{TST+Inf}</math>
|
|- style="background: orange"
|
|<math>\mathsf{NF}+V</math> is [[Total order|linearly ordered]]
<math>\mathsf{NF+PIT}</math>
|
|
|
|- style="background: yellow"
|
|<math>\mathsf{NF}+\mathcal{L}_{\omega_1,\omega}(\omega)</math><ref name="Esser2007relaxing">{{Cite journal 
|  title=Relaxing stratification
|  author=Esser, Olivier and Forster, Thomas
|  journal=Bulletin of the Belgian Mathematical Society-Simon Stevin
|  volume=14
|  number=2
|  pages=247–258
|  year=2007
|  publisher=The Belgian Mathematical Society
| doi=10.36045/bbms/1179839217
|  url=https://www.dpmms.cam.ac.uk/~tef10/relaxing.pdf
|  archiveurl=https://web.archive.org/web/20250813042143/https://www.dpmms.cam.ac.uk/~tef10/relaxing.pdf
|  archivedate=2025-08-13
|  accessdate=2025-08-13
}}</ref>
<math>\mathsf{NF}+</math>the NF set <math>\mathbb{N}\land\mathcal{P}(\mathbb{N})</math> are the real external ones
|
|
|
|-
|<math>\beth_{\beth_{n<\omega}}</math><ref name="HolmesStrongInf" />
<math>\triangleleft\ \beth_{\beth_\omega}</math>
|<math>\mathsf{NFUR}</math>
|
|
|
|-
|
|<math>\mathsf{NFU*}</math><ref>{{Cite web |last=Solovay |first=Robert |date=2025-07-23 |title=The consistency strength of NFU_star |url=https://math.berkeley.edu/~solovay/NFU_star.html |url-status=live |archive-url=https://web.archive.org/web/20250723122841/https://math.berkeley.edu/~solovay/Preprints/new_version.tar.gz |archive-date=2025-07-23 |access-date=2025-07-23}}</ref>
|<math>\mathsf{Z}^- + \Sigma_2\!-\!\mathsf{Replacement}</math>
|
|
|-
|
|<math>\mathsf{NFUA}</math><ref name="HolmesStrongInf" />
|<math>\mathsf{ZFC}+N-\mathsf{Mahlo}</math>
<math>\mathsf{NBG}+N-\mathsf{Mahlo}</math>
|
|
<!--
|-
|
|<math>\mathsf{NFU+CS}</math>{{Citation needed}}
|<math>\mathsf{ZFC}+{n<\omega}-\mathsf{Mahlo}</math>
<math>\mathsf{NBG}+{n<\omega}-\mathsf{Mahlo}</math>
|
|
-->
|-
|
|<math>\mathsf{NFUB}</math><ref name="HolmesStrongInf" />
<math>\mathsf{NFUB}^-</math>
|<math>\mathsf{MK}+\mathbf{Ord}\mathsf{\ is\ weakly\ compact}</math>
<math>\mathsf{ZFC-Pow+}</math>(there is a [[weakly compact cardinal]])
|
|
|-
|
|<math>\mathsf{NFUM}</math><ref name="HolmesStrongInf" />
|<math>\mathsf{MKU}</math>
<math>\mathsf{MK}+\mathbf{Ord}\mathsf{\ is\ measurable}</math>
|<br>
|
|}

=== Key ===
This is a list of symbols used in this table:

* <math>A\triangleleft\ B</math> represents <math>B\vdash \text{Con}(A)</math> .
* <math>A\trianglelefteq B</math> represents <math>\text{Con}(B)\to \text{Con}(A)</math>.
* <math>\mathsf{Inf}</math> in this table only denotes "exist a Dedekind infinite set".

All theories that do not have sufficient information to infer their consistency strength ordering, but whose consistency proofs are explicit, are colored yellow.
All theories without consistency proofs are colored orange.

This is a list of the abbreviations used in this table:

* NF-style set theory
** <math>\mathsf{KF}</math> is a subsystem of both <math>\mathsf{NF}</math> and <math>\mathsf{Z}^-</math>, axiomatized as extensionality, pair set, power set, sumset, and stratified <math>\Delta^\mathcal{P}_0</math> separation. 
** <math>\mathsf{NFI}</math> is a subsystem of <math>\mathsf{NF}</math>, axiomatized as untyped <math>\mathsf{TTI}</math>. 
** <math>\mathsf{NFP}</math> is a subsystem of <math>\mathsf{NF}</math> like <math>\mathsf{NFI}</math>, axiomatized as untyped <math>\mathsf{TTP}</math>. 
** <math>\mathsf{NF}_3</math> is a subsystem of <math>\mathsf{NF}</math>, in which only comprehension is restricted to those formulae which can be stratified using no more than three types. It is not clear whether it is appropriate to put <math>\mathsf{NF}_3</math> on this row.
** <math>\mathsf{NFU}</math> see [[New Foundations#NFU and other variants|NF with urelements]].{{note|NFU1|A}} It is not recommended to read references that are too old and can be read instead <ref name="Adlevsic2024" />
** <math>\mathsf{MLU}</math> is <math>\mathsf{ML}</math> with urelements.
** <math>\mathsf{iNF}</math> the system of set theory that has the same nonlogical axioms as <math>\mathsf{NF}</math> but is embedded in an intuitionistic logic. <math>\mathsf{INF}</math>, <math>\mathsf{iNF}</math>, <math>i\mathsf{NF}</math>, and <math>\mathsf{constructive\ NF}</math> are the same theory.{{note|iNF1|B}} It is not clear whether it is appropriate to put <math>\mathsf{iNF}</math> on this row, because we just have <math>\mathsf{NF}\trianglerighteq\mathsf{iNF}\trianglerighteq\mathsf{NFU}</math> and don't have a proof for <math>\mathsf{iNF}\trianglerighteq\mathsf{HA}</math> and <math>\mathsf{iNF} \vdash \mathsf{Inf}</math>. That is, there might be a largest finite cardinal <math>|U|</math>, which would contain a finite set U that is "unenlargeable", that not exist <math>\mathsf{iNF}</math> set <math>x\not\in U</math>.<ref name="Forster2009">{{Cite journal 
|title=A tutorial on constructive NF
|  author=Forster, Thomas E
|  journal=Proceedings of the 70th Anniversary NF Meeting in Cambridge
|  volume=16
|  year=2009
|url=https://www.dpmms.cam.ac.uk/~tef10/iNF.pdf
|archiveurl=https://web.archive.org/web/20250718112147/https://www.dpmms.cam.ac.uk/~tef10/iNF.pdf
|archivedate=2025-07-18
|accessdate=2025-07-18
}}</ref>
** <math>\mathsf{NF}</math> see [[New Foundations#Definition]].
** <math>\mathsf{ML}</math> is the theory obtained by adding class notion to <math>\mathsf{NF}</math>.<ref>{{Cite book |title=Mathematical logic |last=Quine |first=Willard Van Orman |publisher=Harvard university press |location=Cambridge [Mass.] |date=1976 |isbn=978-0-674-55450-4 |edition=Rev. ed., 8th print}}</ref> Its equiconsistency with <math>\mathsf{NF}</math> implies that we cannot prove anything about classes that are not <math>\mathsf{NF}</math> sets.
** <math>\mathsf{NF(U)+DC}(\alpha)</math> axiomatized as <math>\mathsf{NF}</math> or <math>\mathsf{NFU}</math> plus <math>\mathsf{DC}(\alpha)</math>.
** <math>\mathsf{DC}(\alpha)</math> is defined as follows: Let S be a nonempty set and let R be a binary relation such that for every <math>\alpha</math>-sequence <math>s = \langle x_\gamma : \gamma < \alpha \rangle</math> of elements of S there exists <math>y \in S</math> such that <math>sRy</math>. Then there is a function f such that for every <math>\gamma<\alpha, f(|\gamma)Rf(\gamma)</math>. This axiom is a strengthening of the standard [[Axiom of dependent choice]] because it guarantees the existence of a complete choice sequence of length <math>\alpha</math>, where each step in the sequence is a valid choice based on all previous selections.
** <math>\mathsf{NF}+V</math> is [[Total order|linearly ordered]], There is currently no proof of its consistency.
** <math>\mathsf{NF+PIT}</math> see [[Boolean prime ideal theorem]]. There is currently no proof of its consistency.
** <math>\mathsf{NF}+\mathcal{L}_{\omega_1,\omega}(\omega)</math> is <math>\mathsf{NF}</math> + comprehension for stratified formules of the language <math>\mathcal{L}_{\omega_1,\omega}</math> using only finitely many types. Its model are exactly the models for which the NF set <math>\mathbb{N}\land\mathcal{P}(\mathbb{N})</math> are the real external ones.
** <math>\mathsf{NFUR}</math> axiomatized as <math>\mathsf{NFU+Inf}+\mathbb{N}\mathsf{\ is \ SC}</math>.
** <math>\mathsf{NFU*}</math> axiomatized as <math>\mathsf{NFU+SCS}+\mathbb{N}\mathsf{\ is \ SC}</math>.
** <math>\mathsf{NFUA}</math> axiomatized as <math>\mathsf{NFU+Inf}+\mathsf{C\ is \ SC}</math>.
** <math>\mathsf{NFUB}</math> axiomatized as <math>\mathsf{NFUA+SO}</math>.
** <math>\mathsf{NFUB}^-</math> axiomatized as <math>\mathsf{NFU+Inf}+\mathsf{C\ is \ SC}+\mathsf{SO}</math>.
** <math>\mathsf{NFUM}</math> axiomatized as <math>\mathsf{NFUB}^-+\mathsf{LO}</math>.
** <math>\mathsf{NFU}^{-\infty}</math> axiomatized as <math>\mathsf{NFU}+V</math> is finite.
** <math>\mathsf{NFUA}^{-\infty}</math> axiomatized as <math>\mathsf{NFU}^{-\infty}+\mathsf{C\ is \ SC}</math>.
** <math>\mathsf{NFUB}^{-\infty}</math> axiomatized as <math>\mathsf{NFUA}^{-\infty}+\mathsf{SO}</math>.

The axioms listed below are higher infinite axioms specific to NF-style set theory, and they also apply to NF-style type theory. When used individually, they are not necessarily very strong in the traditional sense (such as <math>\trianglerighteq \text{Con}(\textsf{ZFC})</math>), but when used in combination, they are indeed very strong.
* NF-style higher infinite
** <math>\mathbb{N}\mathsf{\ is \ SC}</math> or <math>\mathsf{Count}</math> is '''Rosser's Axiom of Counting''', which asserts that the set of natural numbers is a strongly Cantorian set.
** <math>\mathsf{SCS}</math> is '''Axiom of strongly Cantorian separation''', which asserts that for any strongly Cantorian set ''A'' and any formula <math>\phi</math> (not necessarily stratified) the set <math>\{x\in A|\;\phi\}</math> exists.
** <math>\mathsf{C\ is\ SC}</math> is '''Axiom of Cantorian Sets''', which asserts that Every Cantorian set is strongly Cantorian.
<!--** <math>\mathsf{CS}</math> is '''Axiom of Cantorian Separation''', which asserts that for any Cantorian set (not necessarily strongly) ''A'' and any formula <math>\phi</math> (not necessarily stratified) the set <math>\{x\in A|\;\phi\}</math> exists.-->
** <math>\mathsf{LO}</math> is '''Axiom of Large Ordinals''', which asserts that for each non-Cantorian ordinal <math>\alpha</math>, there is a natural number ''n'' such that <math>T^n(\Omega) < \alpha</math>.
** <math>\mathsf{SO}</math> is '''Axiom of Small Ordinals''', which asserts that for any formula <math>\phi</math> (not necessarily stratified), there is a set ''A'' such that the elements of ''A'' which are strongly Cantorian ordinals are exactly the strongly Cantorian ordinals such that <math>\phi</math>.
* ZF-style set theory
** <math>\mathsf{MAC}</math> see [[Zermelo set theory#Mac Lane set theory|Mac Lane set theory]].
** <math>\mathsf{MACQ}</math> as <math>\mathsf{MAC}</math> with foundation weakened to allow Quine atoms and an axiom scheme asserting the existence of an n-tree of cardinals for each concrete natural number n.
** '''A tangled web of cardinals''' is a tangled web of cardinals of order <math>\tau</math>. For any infinite ordinal <math>\alpha</math>, a tangled web of cardinals of order <math>\alpha</math> is a function <math>\tau</math> from the set of nonempty sets of ordinals with <math>\alpha</math> as maximum to cardinals such that
# If <math>|A| > 1,\tau(A_1)=2^{\tau(A)}</math>.
# If <math>|A| \leq n</math>, the first order theory of a natural model of <math>\mathsf{TST}_n</math> with base type <math>\tau(A)</math> is completely determined by <math>A \backslash A_n</math>, the n smallest elements of <math>A</math>.
** <math>\mathsf{Z}^-</math> see [[Zermelo set theory]].
** <math>\mathsf{ZFC}</math> see [[Zermelo–Fraenkel set theory]].
** <math>\mathsf{NBG}</math> see [[Von Neumann–Bernays–Gödel set theory]].
** <math>\mathsf{MK}</math> see [[Morse–Kelley set theory]].
** <math>\mathsf{MKU}</math> axiomatized as <math>\mathsf{MK}+</math> "there is a <math>\kappa</math>-complete nonprincipal ultrafilter on the proper class ordinal <math>\kappa</math>".
* Higher infinite
** <math>N-\mathsf{Mahlo}</math> is a schema asserting the existence of an n-Mahlo cardinal for each concrete natural number n, and doesn't prove that n-Mahlo cardinals exist forall n, thus allowing for nonstandard counterexamples.
<!--** <math>n<\omega-\mathsf{Mahlo}</math> asserts that there are n-Mahlo cardinals for every n.-->
** <math>\mathsf{weakly\ compact}</math> see [[weakly compact cardinal]].
** <math>\mathsf{measurable}</math> see [[measurable cardinal]].
* Type-style theory
** <math>\mathsf{FlatOP}</math> see [[New Foundations#Ordered pairs]], is '''Axiom of type-level ordered pair''', which can also be called '''flat ordered pair'''. In models without the [[Axiom of Choice]] <math>\mathsf{AC}</math>, the existence of a type-level ordered pair implies but is not equivalent to the existence of an infinite set, but NFU with the axiom "there is an infinite set" interprets NFU with a type-level pair in a straightforward manner. It's well-known that proofs concerning like <math>\alpha</math>-strong cardinals run into problems if one doesn't use the flat ordered pair, and this is no different from ZF-style set theory.
** <math>\mathsf{Amb}</math> is '''typical ambiguity axiom''', which asserts that validity for closed predicates is invariant under shifts of type levels. 
** <math>\mathsf{TSTI}</math> or <math>\mathsf{TTI}</math> is a subsystem of <math>\mathsf{TST}</math>, axiomatized as unrestricted extensionality and those instances of comprehension in which no variable is assigned a type higher than that of the set asserted to exist.
** <math>\mathsf{TSTP}</math> or <math>\mathsf{TTP}</math> is a subsystem of <math>\mathsf{TST}</math> like <math>\mathsf{TSTI}</math>, in which only free variables are allowed to have the type of the set asserted to exist by an instance of comprehension.
** <math>\mathsf{RTT}</math> axiomatized as [[Principia Mathematica]] [[ramified type theory]] without the [[axiom of reducibility]].
** <math>\mathsf{TTU}</math> is <math>\mathsf{TTT}</math> with urelements, and <math>\mathsf{NFU}</math> is untyped <math>\mathsf{TTU}</math>.
** <math>\mathsf{TSTU}</math> is <math>\mathsf{TST}</math> with urelements, and <math>\mathsf{NFU}</math> is untyped <math>\mathsf{TSTU}</math>.
** <math>\mathsf{T}\mathbb{Z}\mathsf{T}</math> is Simple theory of types with all integer types, it has a realizability model and computational interpretation and is therefore consistent, and <math>\mathsf{iNF}</math> is untyped <math>\mathsf{T}\mathbb{Z}\mathsf{T}</math>.
** <math>\mathsf{TTT}</math> see [[New Foundations#Tangled Type Theory]]. <math>\mathsf{NF}</math> is untyped <math>\mathsf{TTT}</math>.
** <math>\mathsf{TST}</math> or <math>\mathsf{TT}</math> see [[New Foundations#Typed Set Theory]]. <math>\mathsf{NF}</math> is untyped <math>\mathsf{TTT}</math>.
** <math>\mathsf{TST}_k</math> is <math>\mathsf{TST}</math> restricted to levels 0 to k − 1, forall k > 2.
** <math>\mathsf{TST}^\infty_k</math> is <math>\mathsf{TST}_k+</math>"level 0 contains ≥ n things for every concrete n."
** <math>\mathsf{TST}^\infty_3</math> is <math>\mathsf{TST}^\infty_k</math> restricted to k = 3.
* Higher-order arithmetic
** <math>\mathsf{I\Delta_0 + exp}</math> is arithmetic with induction restricted to Δ0-predicates without any axiom asserting that exponentiation is total.
** <math>\mathsf{EFA}</math> see [[elementary function arithmetic]].
** <math>\mathsf{PA}</math> see [[Peano arithmetic]].
** <math>\mathsf{Z}_2</math> see [[Second-order arithmetic]].

==See also==
* [[Alternative set theory]]
* [[Axiomatic set theory]]
* [[Implementation of mathematics in set theory]]
* [[Positive set theory]]
* [[Set-theoretic definition of natural numbers]]

== Notes ==
{{Reflist}}
{{reflist|group=note}}

== References ==
<!--* {{cite journal | last=Forster |first=T. E. |date=2008 | title = The iterative conception of set | journal = The Review of Symbolic Logic | volume = 1 |  pages = 97–110 |doi=10.1017/S1755020308080064 |s2cid=15231169 |url=https://www.dpmms.cam.ac.uk/~tf/iterativeconception.pdf}}-->
* {{citation |mr=1166801 |last=Forster |first=T. E. |date=1992 |title=Set theory with a universal set. Exploring an untyped universe |series=Oxford Science Publications, Oxford Logic Guides |volume=20 |publisher=The Clarendon Press, Oxford University Press |place=New York |isbn=0-19-853395-0}}
* {{cite book |last=Forster | first=T. E. |date=2025 |article-url=http://plato.stanford.edu/entries/quine-nf/ |article=Quine's New Foundations |title=Stanford Encyclopedia of Philosophy}}
* {{cite journal | last1 = Hailperin | first1 = T | year = 1944| title = A set of axioms for logic | journal = [[Journal of Symbolic Logic]] | volume = 9 | issue = 1| pages = 1–19 | doi=10.2307/2267307| jstor = 2267307 | s2cid = 39672836 }}
* {{citation|mr=1759289
|last=Holmes|first= M. Randall
|title=Elementary set theory with a universal set
|series=Cahiers du Centre de Logique |volume= 10|publisher= Université Catholique de Louvain, Département de Philosophie|place= Louvain-la-Neuve|year= 1998|isbn= 2-87209-488-1|url=https://randall-holmes.github.io/head.pdf }}
* {{Cite web |last=Holmes |first=M. Randall |date=2017-05-31 |title=Proof, Sets, and Logic |url=https://randall-holmes.github.io/proofsetslogic.pdf |access-date=2025-08-18 |via=[[GitHub]] |edition=2023}}
<!-- * {{cite journal | doi = 10.1007/s11225-008-9107-8 | volume=88 | issue=2 | title=Symmetry as a Criterion for Comprehension Motivating Quine's 'New Foundations' | year=2008 | journal=Studia Logica | pages=195–213 | last1 = Holmes | first1 = M. Randall| s2cid=207242273 }} -->
* {{citation|title=New Foundations for Mathematical Logic
|first=W. V.|last= Quine
|journal=The American Mathematical Monthly|volume= 44|issue= 2 |year=1937|pages= 70–80
|publisher= Mathematical Association of America
|doi=10.2307/2300564
|jstor=2300564}}
* {{citation|mr=0002508
|last=Quine|first= Willard Van Orman
|title=Mathematical Logic|publisher= W. W. Norton & Co., Inc.|place=New York|year= 1940|edition=first}}
* {{citation|mr=0045661 
|last=Quine|first= Willard Van Orman
|title=Mathematical logic
|edition=Revised |publisher= Harvard University Press|place= Cambridge, Mass.|orig-date=1951|date=1981|isbn=0-674-55451-5 }}
* [[Willard Quine|Quine, W. V.]], 1980, "New Foundations for Mathematical Logic" in ''From a Logical Point of View'', 2nd ed., revised. Harvard Univ. Press: 80–101. The definitive version of where it all began, namely Quine's 1937 paper in the ''American Mathematical Monthly''.

== External links ==
* [http://math.stanford.edu/~feferman/papers/ess.pdf "Enriched Stratified systems for the Foundations of Category Theory"] by [[Solomon Feferman]] (2011)
* [[Stanford Encyclopedia of Philosophy]]:
** [http://plato.stanford.edu/entries/quine-nf Quine's New Foundations] — by Thomas Forster.
** [http://setis.library.usyd.edu.au/stanford/entries/settheory-alternative/ Alternative axiomatic set theories] — by Randall Holmes.
* Randall Holmes: [https://randall-holmes.github.io/nf.html New Foundations Home Page.]
* Randall Holmes: [https://randall-holmes.github.io/Bibliography/setbiblio.html Bibliography of Set Theory with a Universal Set.]
* Randall Holmes: [https://randall-holmes.github.io/Nfproof/newattempt.pdf A new pass at the NF consistency proof]

{{Set theory}}
{{Mathematical logic}}

[[Category:Systems of set theory]]
[[Category:Type theory]]
[[Category:Urelements]]
[[Category:Willard Van Orman Quine]]