New Foundations

In mathematical logic, New Foundations (NF) is a non-well-founded, finitely axiomatizable set theory conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica.

Definition

The well-formed formulas of NF are the standard formulas of propositional calculus with two primitive predicates equality (<math>=</math>) and 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 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 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 finitely axiomatized. One advantage of such a finite axiomatization is that it eliminates the notion of 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. The precise set of axioms can vary, but includes most of the following, with the others provable as theorems:

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>.
This statement can also be viewed as the definition of the equality symbol instead of an axiom. However, in that case another axiom is needed to justify substitution with the equality symbol defined this way.
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>.
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. This can be restricted to the existence of one of the cross products <math>A \times V</math> or <math>V \times B</math>.
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>.
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.
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. This can be defined using the operation of type lowering.
Inclusion: The set <math>[\subseteq] = \{(x, y) | x \subseteq y\}</math> exists. Equivalently, we may consider the set <math>[\in] = [\subseteq] \cap (1 \times V) = \{(\{x\}, y) | x \in y\}</math>.
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.
(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.
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>.
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.
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).
Diagonal: The set <math>[=] = \{(x, x) | x \in V \}</math> exists, called the equality relation.
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.
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.
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>.
Cardinal one: The set <math>1</math> of all singletons, <math>\{ x | \exists y : (\forall w : w \in x \leftrightarrow w = y) \}</math>, exists.
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.
Type lowering: For any set <math>S</math>, the set <math>\text{TL}(S) = \{ z : \forall w : (w, \{z\}) \in S \}</math> exists.

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

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

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

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 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 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 of the singleton map to A, is a set is not only Cantorian set but strongly Cantorian.

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 classes of well-orderings 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 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 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 "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. 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 linearly ordered", NF+PIT, and NF+PP.

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. Hao Wang showed how to amend Quine's axioms for ML so as to avoid this problem.

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 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) 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. 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λ), with NF, and then showing that TTTλ 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, finally resolving the question of NF's consistency.

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>

|<math>\mathsf{NFP}</math>

|<math>\mathsf{TSTP+Inf}</math>

<math>\mathsf{RTT}</math>

|<math>\trianglerighteq\ \mathsf{I\Delta_0 + exp},\mathsf{EFA}</math>

<math>\triangleleft\ \mathsf{PA}</math>

|<math>\mathsf{NFU}</math>

|<math>\mathsf{TST}^\infty_3</math>

|- style="background: yellow"

|<math>\triangleleft\ \beth_{\omega_1}</math>

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

|<math>\mathrm{KPu}^r</math>p. 869

|<math>\mathsf{PA}</math>

|<math>\beth_{n<\omega}</math>

<math>\triangleleft\ \beth_{\omega}</math>

|<math>\mathsf{NFU+Inf}</math>, <math>\mathsf{MLU+Inf}</math>

|<math>\mathsf{TTTU+FlatOP}</math>

<math>\mathsf{TSTU+FlatOP}</math>

<math>\mathsf{TTTU+Inf}</math>

<math>\mathsf{TSTU+Inf}</math>

|<math>\mathsf{NFI}</math>

|<math>\mathsf{KP}+\Pi_\omega^{\text{set-\mathsf{Separation}</math>

|<math>\mathsf{TSTI+Inf}</math>

|<math>\mathsf{Z}_2</math>,<math>\Pi^1_\infty - \mathsf{CA}</math>

|<math>\trianglerighteq\beth_\omega</math>

<math>\triangleleft\ \beth_{\omega_1}</math>

|<math>\mathsf{NF}</math>, <math>\mathsf{ML}</math>

<math>\mathsf{KF}+\exists</math> Universal set

<math>\mathsf{NFI}</math> + Axiom of union, <math>\mathsf{NFP}</math> + Axiom of union

<math>\mathsf{NF}_4</math>, <math>\mathsf{NF}_3+</math>(there exists the set <math>\{\{\{x\}, y\}/x\in y\}</math>)

|<math>\mathsf{MACQ}</math>

|<math>\mathsf{TTT}</math>

<math>\mathsf{TST+Amb}</math>

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

|<math>\mathsf{Z}^- + \Sigma_2\!-\!\mathsf{Replacement}</math>

|<math>\mathsf{NFUA}</math>

|

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 NF with urelements.
<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.
<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>. 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 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{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 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>\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.

Notes

Citations

References

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

"Enriched Stratified systems for the Foundations of Category Theory" by Solomon Feferman (2011)
Stanford Encyclopedia of Philosophy:
Quine's New Foundations — by Thomas Forster.
Alternative axiomatic set theories — by Randall Holmes.
Randall Holmes: New Foundations Home Page.
Randall Holmes: Bibliography of Set Theory with a Universal Set.
Randall Holmes: A new pass at the NF consistency proof