New Foundations


In mathematical logic, New Foundations is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name. Much of this entry discusses NFU, an important variant of NF due to Jensen and exposited in Holmes. In 1940 and in a revision of 1951, Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included proper classes as well as sets.
New Foundations has a universal set, so it is a non-well-founded set theory. That is to say, it is an axiomatic set theory that allows infinite descending chains of membership such as
… xn ∈ xn-1 ∈ … ∈ x2 ∈ x1. It avoids Russell's paradox by permitting only stratifiable formulas to be defined using the axiom schema of comprehension. For instance x ∈ y is a stratifiable formula, but x ∈ x is not.

The type theory TST

The primitive predicates of Russellian unramified typed set theory, a streamlined version of the theory of types, are equality and membership. TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each natural number n, type n+1 objects are sets of type n objects; sets of type n have members of type n-1. Objects connected by identity must have the same type. The following two atomic formulas succinctly describe the typing rules: and.
The axioms of TST are:
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 type. In 1914, Norbert Wiener showed how to code the ordered pair as a set of sets, making it possible to eliminate relation types in favor of the linear hierarchy of sets described here.

Quinean set theory

Axioms and stratification

The well-formed formulas of New Foundations are the same as the well-formed formulas of TST, but with the type annotations erased. The axioms of NF are:
By convention, NF's Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. A formula is said to be stratified if there exists a function f from pieces of syntax to the natural numbers, such that for any atomic subformula of we have f = f + 1, while for any atomic subformula of, we have f = f. Comprehension then becomes:
Even the indirect reference to types implicit in the notion of stratification can be eliminated. Theodore Hailperin showed in 1944 that Comprehension is equivalent to a finite conjunction of its instances, so that NF can be finitely axiomatized without any reference to the notion of type.
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 is not an axiom of NF, because cannot be stratified.

Ordered pairs

and functions are defined in TST as sets of ordered pairs in the usual way. The usual definition of the ordered pair, first proposed by Kuratowski in 1921, has a serious drawback for NF and related theories: the resulting ordered pair necessarily has a type two higher than the type of its arguments. 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 type as that of its arguments, 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. Holmes takes the ordered pair and its left and right projections as primitive. Fortunately, whether the ordered pair is type-level by definition or by assumption usually does not matter.
The existence of a type-level ordered pair implies Infinity, and NFU + Infinity interprets NFU + "there is a type level ordered pair". Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair.

Admissibility of useful large sets

NF allow the construction of two kinds of sets that ZFC and its proper extensions disallow because they are "too large" :
New Foundations can be finitely axiomatized.

Cartesian closure

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

The consistency problem and related partial results

For many years, the outstanding problem with NF has been that it has not conclusively been proved to be relatively consistent to any other well-known axiomatic system in which arithmetic can be modelled. NF disproves Choice, and thus proves Infinity. But it is also known that allowing urelements yields NFU, a theory that is consistent relative to Peano arithmetic; if Infinity and Choice are added, the resulting theory has the same consistency strength as type theory with infinity or bounded Zermelo set theory. There are other relatively consistent variants of NF.
NFU is, roughly speaking, weaker than NF because in NF, the power set of the universe is the universe itself, while in NFU, the power set of the universe may be strictly smaller than the universe. In fact, this is necessarily the case in NFU+"Choice".
Specker has shown that NF is equiconsistent with TST + Amb, where Amb is the axiom scheme of typical ambiguity which asserts for any formula, being the formula obtained by raising every type index in by one. NF is also equiconsistent with the theory TST augmented with a "type shifting automorphism", an operation which raises type by one, mapping each type onto the next higher type, and preserves equality and membership relations. The same results hold for various fragments of TST in relation to the corresponding fragments of NF.
In the same year that Jensen proved NFU consistent, Grishin proved consistent. is the fragment of NF with full extensionality and those instances of Comprehension which can be stratified using just three types. This theory is a very awkward medium for mathematics, largely because there is no obvious definition for an ordered pair. Despite this awkwardness, is very interesting because every infinite model of TST restricted to three types satisfies Amb. Hence for every such model there is a model of with the same theory. This does not hold for four types: is the same theory as NF, and we have no idea how to obtain a model of TST with four types in which Amb holds.
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. Crabbé also discussed a subtheory of NFI, in which only parameters are allowed to have the type of the set asserted to exist by an instance of Comprehension. He called the result "predicative NF" ; it is, of course, doubtful whether any theory with a self-membered universe is truly predicative. Holmes has shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the Axiom of reducibility.
Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF have been available both on arxiv and on the logician's home page. Holmes demonstrates the equiconsistency of a 'weird' variant of TST, namely TTTλ - 'tangled type theory with λ-types' - with NF. Holmes next shows that TTTλ is consistent relative to ZFA, that is, ZF with atoms but without choice. Holmes demonstrates this by constructing in ZFA+C, that is, ZF with atoms and choice, a class model of ZFA which includes 'tangled webs of cardinals'. The candidate proofs are all rather long, but no irrecoverable faults have been identified by the NF community as yet.

How NF(U) avoids the set-theoretic paradoxes

NF steers clear of the three well-known paradoxes of set theory. That NFU, a consistent theory, also avoids the paradoxes may increase one's confidence in this fact.
The Russell paradox: An easy matter; is not a stratified formula, so the existence of is not asserted by any instance of Comprehension. Quine said that he constructed NF with this paradox uppermost in mind.
Cantor's paradox of the largest cardinal number exploits the application of Cantor's theorem to the universal set. Cantor's theorem says that the power set of any set is larger than . Now of course there is an injection from into, if is the universal set! The resolution requires that one observes that makes no sense in the theory of types: the type of is one higher than the type of. The correctly typed version is, where is the set of one-element subsets of. The specific instance of this theorem of interest is : there are fewer one-element sets than sets. The "obvious" bijection 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 ; Choice allows one not only to prove that there are urelements but that there are many cardinals between and.
One can now introduce some useful notions. A set which satisfies the intuitively appealing is said to be Cantorian: a Cantorian set satisfies the usual form of Cantor's theorem. A set which satisfies the further condition that, the restriction of the singleton map to A, is a set is not only Cantorian set but strongly Cantorian.
The Burali-Forti paradox of the largest ordinal number goes as follows. Define the ordinals as equivalence classes of well-orderings under isomorphism. There is an obvious natural well-ordering on the ordinals; since it is a well-ordering it belongs to an ordinal. It is straightforward to prove that the order type of the natural order on the ordinals less than a given ordinal is itself. But this means that is the order type of the ordinals and so is strictly less than the order type of all the ordinals — but the latter is, by definition, itself!
The solution to the paradox in NF starts with the observation that the order type of the natural order on the ordinals less than is of a higher type than. Hence a type level ordered pair is two types higher than the type of its arguments and the usual Kuratowski ordered pair four types higher. For any order type, we can define an order type one type higher: if, then is the order type of the order. The triviality of the T operation is only a seeming one; it is easy to show that T is a strictly monotone operation on the ordinals.
Now the lemma on order types may be restated in a stratified manner: the order type of the natural order on the ordinals is or
depending on which pair is used. From this one may deduce that the order type on the ordinals is, and thus . Hence the T operation is not a function; there cannot be a strictly monotone set map from ordinals to ordinals which sends an ordinal downward! Since T is monotone, we have, a "descending sequence" in the ordinals which cannot be a set.
One might assert that this result shows that no model of NF is "standard", since the ordinals in any model of NFU are externally not well-ordered. One need not take a position on this, but can note that it is also a theorem of NFU that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe V is a model of NFU, despite 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 system ML (Mathematical Logic)

ML is an extension of NF that includes proper classes as well as sets.
The set theory of the 1940 first edition of Quine's Mathematical Logic married NF to the proper classes of NBG set theory, and included an axiom schema of unrestricted comprehension for proper classes. However proved that the system presented in Mathematical Logic was subject to the Burali-Forti paradox. This result does not apply to NF. showed how to amend Quine's axioms for ML so as to avoid this problem, and Quine included the resulting axiomatization in the 1951 second and final edition of Mathematical Logic.
Wang proved that if NF is consistent then so is the revised ML, and also showed that the revised ML can prove the consistency of NF, that is that NF and the revised ML are equiconsistent.

Models of NFU

There is 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 on which there is an external automorphism j which moves a rank of the cumulative hierarchy of sets. We may suppose without loss of generality that. We talk about the automorphism moving the rank rather than the ordinal because we do not want to assume that every ordinal in the model is the index of a rank.
The domain of the model of NFU will be the nonstandard rank. The membership relation of the model of NFU will be
It may now be proved that this actually is a model of NFU. Let 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 into a formula 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 in such a way that each variable x assigned type i occurs with exactly 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 can be converted to the form . Carry out this transformation everywhere and obtain a formula in which j is never applied to a bound variable.
Choose any free variable y in assigned type i. Apply uniformly to the entire formula to obtain a formula in which y appears without any application of j. Now exists, belongs to, and contains exactly those y which satisfy the original formula
in the model of NFU. has this extension 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 inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.
The basic idea is that the automorphism j codes the "power set" of our "universe" into its externally isomorphic copy inside our "universe." The remaining objects not coding subsets of the universe are treated as urelements.
If is a natural number n, one gets a model of NFU which claims that the universe is finite. If is infinite and the Choice holds in the nonstandard model of ZFC, one obtains a model of NFU + Infinity + Choice.

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 outline: take the type theory TSTU as a metatheory and consider the theory of set models of TSTU in TSTU. Given an embedding of into , embeddings may be defined from each "type" into its successor in a natural way. This can be generalized to transfinite sequences 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. 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 's being used in place of 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 which is also a well-ordering in NFU, and W has type α in NFU, then j 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 to its sole element, becomes in NFU a function which sends each singleton, where x is any object in the universe, to j. 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 = 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.

Strong axioms of infinity

In this section, the effect is considered of adding various "strong axioms of infinity" to our usual base theory, NFU + Infinity + Choice. This base theory, known consistent, has the same strength as TST + Infinity, or Zermelo set theory with Separation restricted to bounded formulas.
One can add to this base theory strong axioms of infinity familiar from the ZFC context, such as "there exists an inaccessible cardinal," but it is more natural to consider assertions about Cantorian and strongly Cantorian sets. Such assertions not only bring into being large cardinals of the usual sorts, but strengthen the theory on its own terms.
The weakest of the usual strong principles is:
To see how natural numbers are defined in NFU, see set-theoretic definition of natural numbers. The original form of this axiom given by Rosser was "the set has n members", for each natural number n. This intuitively obvious assertion is unstratified: what is provable in NFU is "the set has members". For any cardinal number to assert is equivalent to asserting that the sets A of that cardinality are Cantorian. It is straightforward to show that the assertion that each natural number is Cantorian is equivalent to the assertion that the set of all natural numbers is strongly Cantorian.
Counting is consistent with NFU, but increases its consistency strength noticeably; not, as one would expect, in the area of arithmetic, but in higher set theory. NFU + Infinity proves that each exists, but not that exists; NFU + Counting proves Infinity, and further proves the existence of for each n, but not the existence of..
Counting implies immediately that one does not need to assign types to variables restricted to the set of natural numbers for purposes of stratification; it is a theorem that the power set of a strongly Cantorian set is strongly Cantorian, so it is further not necessary to assign types to variables restricted to any iterated power set of the natural numbers, or to such familiar sets as the set of real numbers, the set of functions from reals to reals, and so forth. The set-theoretical strength of Counting is less important in practice than the convenience of not having to annotate variables known to have natural number values with singleton brackets, or to apply the T operation in order to get stratified set definitions.
Counting implies Infinity; each of the axioms below needs to be adjoined to NFU + Infinity to get the effect of strong variants of Infinity; Ali Enayat has investigated the strength of some of these axioms in models of NFU + "the universe is finite".
A model of the kind constructed above satisfies Counting just in case the automorphism j fixes all natural numbers in the underlying nonstandard model of Zermelo set theory.
The next strong axiom we consider is the
Immediate consequences include Mathematical Induction for unstratified conditions.
This axiom is surprisingly strong. Unpublished work of Robert Solovay shows that the consistency strength of the theory NFU* = NFU + Counting + Strongly Cantorian Separation is the same as that of Zermelo set theory + Replacement.
This axiom holds in a model of the kind constructed above if the ordinals which are fixed by j and dominate only ordinals fixed by j in the underlying nonstandard model of Zermelo set theory are standard, and the power set of any such ordinal in the model is also standard. This condition is sufficient but not necessary.
Next is
This very simple and appealing assertion is extremely strong. Solovay has shown the precise equivalence of the consistency strength of the theory NFUA = NFU + Infinity + Cantorian Sets with that of ZFC + a schema asserting the existence of an n-Mahlo cardinal for each concrete natural number n. Ali Enayat has shown that the theory of Cantorian equivalence classes of well-founded extensional relations interprets the extension of ZFC with n-Mahlo cardinals directly. A permutation technique can be applied to a model of this theory to give a model in which the hereditarily strongly Cantorian sets with the usual membership relation model the strong extension of ZFC.
This axiom holds in a model of the kind constructed above just in case the ordinals fixed by j in the underlying nonstandard model of ZFC are an initial segment of the ordinals of the model.
Next consider the
This combines the effect of the two preceding axioms and is actually even stronger. Unstratified mathematical induction enables proving that there are n-Mahlo cardinals for every n, given Cantorian Sets, which gives an extension of ZFC that is even stronger than the previous one, which only asserts that there are n-Mahlos for each concrete natural number.
This axiom will hold in a model of the kind described above if every ordinal fixed by j is standard, and every power set of an ordinal fixed by j is also standard in the underlying model of ZFC. Again, this condition is sufficient but not necessary.
An ordinal is said to be Cantorian if it is fixed by T, and strongly Cantorian if it dominates only Cantorian ordinals. In models of the kind constructed above, Cantorian ordinals of NFU correspond to ordinals fixed by j.
Equal in strength to Cantorian Sets is the
Recall that is the order type of the natural order on all ordinals. This only implies Cantorian Sets if we have Choice. It is remarkable that one can even define : this is the nth term of any finite sequence of ordinals s of length n such that, for each appropriate i. This definition is completely unstratified. The uniqueness of can be proved and a certain amount of common-sense reasoning about this notion can be carried out, enough to show that Large Ordinals implies Cantorian Sets in the presence of Choice. In spite of the knotty formal statement of this axiom, it is a very natural assumption, amounting to making the action of T on the ordinals as simple as possible.
A model of the kind constructed above will satisfy Large Ordinals, if the ordinals moved by j are exactly the ordinals which dominate some in the underlying nonstandard model of ZFC.
Solovay has shown the precise equivalence in consistency strength of NFUB = NFU + Infinity + Cantorian Sets + Small Ordinals with Morse–Kelley set theory plus the assertion that the proper class ordinal is a weakly compact cardinal. This is very strong indeed! Moreover, NFUB-, which is NFUB with Cantorian Sets omitted, is easily seen to have the same strength as NFUB.
A model of the kind constructed above will satisfy this axiom if every collection of ordinals fixed by j is the intersection of some set of ordinals with the ordinals fixed by j, in the underlying nonstandard model of ZFC.
Even stronger is the theory NFUM = NFU + Infinity + Large Ordinals + Small Ordinals. This is equivalent to Morse–Kelley set theory with a predicate on the classes which is a κ-complete nonprincipal ultrafilter on the proper class ordinal κ; in effect, this is Morse–Kelley set theory + "the proper class ordinal is a measurable cardinal"!
The technical details here are not the main point, which is that reasonable and natural assertions turn out to be equivalent in power to very strong axioms of infinity in the ZFC context. This fact is related to the correlation between the existence of models of NFU, described above and satisfying these axioms, and the existence of models of ZFC with automorphisms having special properties.