New Foundations

The well-formed formulas of New Foundations (NF) are the same as the well-formed formulas of TST, but with the type annotations erased. The axioms of NF are:

• Extensionality: Two objects with the same elements are the same object;
• A comprehension schema: All instances of TST Comprehension but with type indices dropped (and without introducing new identifications between variables).

By convention, NF's Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. A formula ${\displaystyle \phi }$ is said to be stratified if there exists a function f from pieces of ${\displaystyle \phi }$'s syntax to the natural numbers, such that for any atomic subformula ${\displaystyle x\in y}$ of ${\displaystyle \phi }$ we have f(y) = f(x) + 1, while for any atomic subformula ${\displaystyle x=y}$ of ${\displaystyle \phi }$, we have f(x) = f(y). Comprehension then becomes:

${\displaystyle \{x\mid \phi \}}$ exists for each stratified formula ${\displaystyle \phi }$.

Comprehension 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 ${\displaystyle \{x\mid x\not \in x\}}$ is not an axiom of NF, because ${\displaystyle x\not \in x}$ cannot be stratified.

Theodore Hailperin showed in 1944 that Comprehension is equivalent to a finite conjunction of its instances,[4] so NF can be finitely axiomatized. One advantage of such a finite axiomatization is that it eliminates the indirect reference to types through the notion of stratification. The Metamath database for New Foundations on the Metamath website[5] implements Hailperin's finite axiomatization.

Holmes believes that the axiom of stratified comprehension, while a powerful tool, is not at all intuitive compared to the axioms in a finite axiomatization, which all correspond to natural basic constructions.[6] Therefore, in his introduction to NFU, he opted to take those natural basic constructions as axioms, and proved stratified comprehension as a theorem later.

Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way. The usual definition of the ordered pair, first proposed by Kuratowski in 1921, namely ${\displaystyle (a,\ b)_{K}\;:=\ \{\{a\},\ \{a,\ b\}\}}$, has a serious drawback for NF and related theories: the resulting ordered pair (a, b) necessarily has 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.

If one can define a pair in such a way that its type is the same as that of its arguments (resulting in a type-level ordered pair), then a relation or function is merely one type higher than the type of the members of its field. Hence NF and related theories usually employ 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[2] takes the ordered pair (a, b) as a primitive notion, as well as its left and right projections ${\displaystyle \pi _{1}}$ and ${\displaystyle \pi _{2}}$, i.e., functions such that ${\displaystyle \pi _{1}((a,b))=a}$ and ${\displaystyle \pi _{2}((a,b))=b}$ (in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of ${\displaystyle \{x\mid \phi \}}$ for any stratified formula ${\displaystyle \phi }$ is considered a theorem and only proved later, so expressions like ${\displaystyle \pi _{1}=\{((a,b),a)\mid a,b\in V\}}$ 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.

The usual form of the axiom of infinity is based on the 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 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 ${\displaystyle \{\varnothing \}}$, and the successor operation can be defined in a stratified way:

${\displaystyle S(A)=\{a\cup \{x\}\mid a\in A\wedge x\notin a\}.}$

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 ${\displaystyle V}$ would be an inductive set.

Since inductive sets always exist, the set of natural numbers ${\displaystyle \mathbf {N} }$ can be defined as the intersection of all inductive sets. This definition enables mathematical induction for stratified statements ${\displaystyle P(n)}$, because the set ${\displaystyle \{n\in \mathbf {N} \mid P(n)\}}$ can be constructed, and when ${\displaystyle P(n)}$ 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 ${\displaystyle V}$ is not a "finite set", i.e., that the size of the universe ${\displaystyle |V|}$ is not a natural number. Suppose that ${\displaystyle |V|=n\in \mathbf {N} }$. Then ${\displaystyle n=\{V\}}$ (it can be shown inductively that a finite set is not equinumerous with any of its proper subset), ${\displaystyle n+1=S(n)=\varnothing }$, and each subsequent natural number would be ${\displaystyle \varnothing }$ too, causing arithmetic to break down. To prevent this, one can introduce the axiom of infinity for NF:

${\displaystyle \varnothing \notin \mathbf {N} .}$[7]

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 ${\displaystyle \varnothing ,\{\varnothing \},\{\{{\varnothing }\}\},\ldots }$. 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 logically independent of NFU: There exists models of NFU where ${\displaystyle |V|}$ is a non-standard natural number. In such models, mathematical induction can prove statements about ${\displaystyle |V|}$, making it impossible to "distinguish" ${\displaystyle |V|}$ 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 urelements), Specker[8] 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 ${\displaystyle V}$ is infinite.
• In NFU with axioms asserting the existence of a type-level ordered pair, ${\displaystyle V}$ is equinumerous with its proper subset ${\displaystyle V\times \{0\}}$, which implies Infinity.[7] 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).

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 classes):

• The universal set V. Because ${\displaystyle x=x}$ is a stratified formula, the universal set V = {x | x=x} exists by Comprehension. An immediate consequence is that all sets have complements, and the entire set-theoretic universe under NF has a Boolean structure.
• Cardinal and ordinal numbers. In NF (and TST), the set of all sets having n elements (the 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 of equinumerosity: the sets A and B are equinumerous if there exists a bijection between them, in which case we write ${\displaystyle A\sim B}$. Likewise, an ordinal number is an equivalence class of well-ordered sets.

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. Of course, one may have doubts about whether those unfamiliar concepts would inherently cause inconsistencies down the line, especially since they did lead to some surprising results, e.g., that NF disproves Choice (in other words, NF+Choice is inconsistent). However, the fact that NFU, a consistent (relative to Peano arithmetic) theory that is consistent with Choice, also avoids the paradoxes in similar ways may relieve such doubts.

The resolution of Russell's paradox is trivial: ${\displaystyle x\not \in x}$ is not a stratified formula, so the existence of ${\displaystyle \{x\mid x\not \in x\}}$ is not asserted by any instance of Comprehension. Quine said that he constructed NF with this paradox uppermost in mind.[9] The resolution of the two more technical paradoxes, Cantor's paradox and the Burali-Forti paradox, is more involved.

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 ${\displaystyle V}$ is obviously a set with the largest cardinality. However, Cantor's theorem says (given ZFC) that the power set ${\displaystyle P(A)}$ of any set ${\displaystyle A}$ is larger than ${\displaystyle A}$ (there can be no injection (one-to-one map) from ${\displaystyle P(A)}$ into ${\displaystyle A}$), which seems to imply a contradiction when ${\displaystyle A=V}$.

Of course there is an injection from ${\displaystyle P(V)}$ into ${\displaystyle V}$ since ${\displaystyle V}$ 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 ${\displaystyle B=\{x\in A\mid x\notin f(x)\}}$. In NF, ${\displaystyle x}$ and ${\displaystyle f(x)}$ should be assigned the same type, so the definition of ${\displaystyle B}$ is not stratified. Indeed, if ${\displaystyle f:P(V)\to V}$ is the trivial injection ${\displaystyle x\mapsto x}$, then ${\displaystyle B}$ is the same (ill-defined) set in Russell's paradox.

This failure is not surprising since ${\displaystyle |A|<|P(A)|}$ makes no sense in TST: the type of ${\displaystyle P(A)}$ is one higher than the type of ${\displaystyle A}$. In NF, ${\displaystyle |A|<|P(A)|}$ 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 ${\displaystyle A}$ with ${\displaystyle P_{1}(A)}$, the set of one-element subsets of ${\displaystyle A}$. Indeed, the correctly typed version of Cantor's theorem ${\displaystyle |P_{1}(A)|<|P(A)|}$ is a theorem in TST (thanks to the diagonalization argument), and thus also a theorem in NF. In particular, ${\displaystyle |P_{1}(V)|<|P(V)|}$: 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 ${\displaystyle x\mapsto \{x\}}$ 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 known models of NFU it is the case that ${\displaystyle |P_{1}(V)|<|P(V)|\ll |V|}$; Choice allows one not only to prove that there are urelements but that there are many cardinals between ${\displaystyle |P(V)|}$ and ${\displaystyle |V|}$.

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

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 ${\displaystyle \Omega }$ that corresponds to the natural well-ordering of all ordinals, but that does not mean that ${\displaystyle \Omega }$ 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 ${\displaystyle \mathrm {Ord} }$ can be defined with no problem. Transfinite induction works on stratified statements, which allows one to prove that the natural ordering of ordinals (${\displaystyle \alpha \leq \beta }$ iff there exists well-orderings ${\displaystyle R\in \alpha ,S\in \beta }$ such that ${\displaystyle S}$ is a continuation of ${\displaystyle R}$) is an well-ordering of ${\displaystyle \mathrm {Ord} }$. By definition of ordinals, this well-ordering also belongs to an ordinal ${\displaystyle \Omega \in \mathrm {Ord} }$. In naive set theory, one would go on to prove by transfinite induction that each ordinal ${\displaystyle \alpha }$ is the order type of the natural order on the ordinals less than ${\displaystyle \alpha }$, which would imply an contradiction since ${\displaystyle \Omega }$ by definition is the order type of all ordinals, not any proper initial segment of them.

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

To correct such a type problem, one needs the T operation, ${\displaystyle T(\alpha )}$, that "raises the type" of an ordinal ${\displaystyle \alpha }$, just like how ${\displaystyle P_{1}(A)}$ "raises the type" of the set ${\displaystyle A}$. The T operation is defined as follows: If ${\displaystyle W\in \alpha }$, then ${\displaystyle T(\alpha )}$ is the order type of the order ${\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}}$. Now the lemma on order types may be restated in a stratified manner:

The order type of the natural order on the ordinals ${\displaystyle <\alpha }$ is ${\displaystyle T^{2}(\alpha )}$ or ${\displaystyle T^{4}(\alpha )}$, 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 ${\displaystyle T^{2}(\alpha )}$ is always less than ${\displaystyle \Omega }$, the order type of all ordinals. In particular, ${\displaystyle T^{2}(\Omega )<\Omega }$.

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., ${\displaystyle T(\alpha )<T(\beta )}$ iff ${\displaystyle \alpha <\beta }$. Hence the T operation is not a function: The collection of ordinals ${\displaystyle \{\alpha \mid T(\alpha )<\alpha \}}$ cannot have a least member, and thus cannot be a set. More concretely, the monotonicity of T implies ${\displaystyle \Omega >T^{2}(\Omega )>T^{4}(\Omega )\ldots }$, 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 ${\displaystyle V}$ is a model of NFU, despite ${\displaystyle V}$ being a set, because the membership relation is not a set relation.

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.

The category whose objects are the sets of NF and whose arrows are the functions between those sets is not Cartesian closed;[11] Since NF lacks Cartesian closure, not every function curries as one might intuitively expect, and NF is not a topos.

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 ${\displaystyle T_{i}}$ (all of the same type in the metatheory) with embeddings of each ${\displaystyle P(T_{i})}$ into ${\displaystyle P_{1}(T_{i+1})}$ coding embeddings of the power set of ${\displaystyle T_{i}}$ into ${\displaystyle T_{i+1}}$ in a type-respecting manner). Given an embedding of ${\displaystyle T_{0}}$ into ${\displaystyle T_{1}}$ (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 ${\displaystyle T_{\alpha }}$ 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 ${\displaystyle \beth _{\omega }}$, 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 ${\displaystyle T_{\alpha }}$'s being used in place of ${\displaystyle V_{\alpha }}$ 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.

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 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 urelements 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 ${\displaystyle V_{j(\alpha )}}$ 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 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.