In mathematical logic, New Foundations (NF) 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 (1969) and exposited in Holmes (1998). In 1940 and 1951 Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included classes as well as sets.
Contents
- The type theory TST
- Axioms and stratification
- Ordered pairs
- Admissibility of useful large sets
- Finite axiomatizability
- Cartesian closure
- The consistency problem and related partial results
- How NFU avoids the set theoretic paradoxes
- The system ML Mathematical Logic
- Models of NFU
- Self sufficiency of mathematical foundations in NFU
- Facts about the automorphism j
- Strong axioms of infinity
- References
New Foundations has a universal set, so it is a non well founded set theory. That is to say, it is a logical theory that allows infinite descending chains of membership such as … xn ∈ xn-1 ∈ …x3 ∈ x2 ∈ x1. It avoids Russell's paradox by only allowing stratifiable formulae in the axiom of comprehension. For instance x ∈ y is a stratifiable formula, but x ∈ x is not (for details of how this works see below).
The type theory TST
The primitive predicates of Russellian unramified typed set theory (TST), a streamlined version of the theory of types, are equality (
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.
Axioms and stratification
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:
By convention, NF's Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. A formula
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
Ordered pairs
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, 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 (its left and right projections). 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 (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. Holmes (1998) 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 (i.e., taken as primitive) 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" (they are not quite the same theory, but the differences are inessential). Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair.
Admissibility of useful 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 classes):
Finite axiomatizability
New Foundations can be finitely axiomatized.
Cartesian closure
Unfortunately, the category whose objects are the sets of NF and whose morphisms are the functions between those sets is not cartesian closed; this is a highly desirable property for any set theory to have. Intuitively, it means that the functions of NF do not curry as one would normally expect functions to. Furthermore, it means that NF is not a topos.
The consistency problem and related partial results
The outstanding problem with NF is that it is not known to be relatively consistent to any mainstream mathematical system. NF disproves Choice, and so proves Infinity (Specker, 1953). But it is also known (Jensen, 1969) that allowing urelements (multiple distinct objects lacking members) 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. (NFU corresponds to a type theory TSTU, where type 0 has urelements, not just a single empty set.) 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 (the power set of the universe contains only sets, while the universe may contain urelements). 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
In the same year (1969) that Jensen proved NFU consistent, Grishin proved
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. Holmes has shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the Axiom of reducibility.
How NF(U) avoids the set-theoretic paradoxes
NF steers clear of the three well-known paradoxes of set theory. That NFU, a consistent (relative to Peano arithmetic) theory, also avoids the paradoxes increases our confidence in this fact.
The Russell paradox: An easy matter;
Cantor's paradox of the largest cardinal number exploits the application of Cantor's theorem to the universal set. Cantor's theorem says (given ZFC) that the power set
We now introduce some useful notions. A set
The Burali-Forti paradox of the largest ordinal number goes as follows. We define (following naive set theory) 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
The solution to the paradox in NF(U) starts with the observation that the order type of the natural order on the ordinals less than
We can now restate the lemma on order types in a stratified manner: the order type of the natural order on the ordinals
Some have asserted 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. We do not take a position on this, but we 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 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 J. Barkley Rosser (1942) proved that the system presented in Mathematical Logic was subject to the Burali-Forti paradox. This result does not apply to NF. Hao Wang (1950) showed how to amend Quine's axioms 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 ML, and also showed that ML can prove the consistency of NF.
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 (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
The domain of the model of NFU will be the nonstandard rank
We now prove that this actually is a model of NFU. Let
Expand the formula
Choose any free variable y in
To see that weak Extensionality holds is straightforward: each nonempty element of
The basic idea is that the automorphism j codes the "power set"
If
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 our reasons for relying on it have to do with our intuition that ZFC is correct. We claim that it is sufficient to accept TST (in fact TSTU). We outline the approach: take the type theory TSTU (allowing urelements in each positive type) as our metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets
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
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 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
Strong axioms of infinity
In this section we mainly discuss the effect 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 (Mac Lane set theory).
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 {m|1≤m≤n} has n members", for each natural number n. This intuitively obvious assertion is unstratified: what is provable in NFU is "the set {m|1≤m≤n} has
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
Counting implies immediately that one does not need to assign types to variables restricted to the set
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 (which is not a consequence of Counting; many but not all unstratified instances of induction on the natural numbers follow from Counting).
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 +
This axiom holds in a model of the kind constructed above (with Choice) 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 (which gives a natural picture of an initial segment of the cumulative hierarchy of ZFC) 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 (with Choice) just in case the ordinals fixed by j in the underlying nonstandard model of ZFC are an initial (proper class) segment of the ordinals of the model.
Next consider the
This combines the effect of the two preceding axioms and is actually even stronger (precisely how is not known). 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 (leaving open the possibility of nonstandard counterexamples).
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 (this implies that it is itself Cantorian). In models of the kind constructed above, Cantorian ordinals of NFU correspond to ordinals fixed by j (they are not the same objects because different definitions of ordinal numbers are used in the two theories).
Equal in strength to Cantorian Sets is the
Recall that
A model of the kind constructed above will satisfy Large Ordinals, if the ordinals moved by j are exactly the ordinals which dominate some
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 (the class of all ordinals) 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 (in the context of NFU) 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.