New Foundations
From Free net encyclopedia
In mathematical logic, New Foundations (NF) is a candidate set theory proposed by Willard van Orman Quine, obtained from a streamlined version of the theory of types of Bertrand Russell. It is so called because it was proposed in an article entitled New Foundations for mathematical logic, which appeared in American Mathematical Monthly, February, 1937.
Contents |
The type theory TST
The streamlined version of the theory of types (which we call TST) has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed, while for each (meta-) natural number n, type n+1 objects are understood to be sets of type n objects. The primitive predicates of this theory are equality and membership. Typing rules for well-formed atomic sentences are succinctly summed up in the formulas <math>x^{n} = y^{n}</math> and <math>x^{n} \in y^{n+1}</math> (notation to be improved). The original type theory of the Principia Mathematica of Bertrand Russell and Alfred North Whitehead implemented a much more complex type system including types of relations with possibly heterogeneous argument types. In 1914, Norbert Wiener discovered that the ordered pair can be coded as a set, and so it is possible to eliminate relation types in favor of a linear hierarchy of types of sets as described here. The usual definition of the ordered pair as a set is not that of Norbert Wiener but a later one due to Kuratowski. In NF, one frequently uses another definition of ordered pair due to Quine.
The axioms of the theory TST are extensionality (sets of the same (positive) type with the same members are equal) and a comprehension schema:
- <math>\{x^n \mid \phi(x^n)\}^{n+1}</math> exists
for any well-formed formula <math>\phi(x^n)</math>: i.e., for any such formula <math>\phi(x^n)</math> there is a set <math>A^{n+1}</math> such that for all <math>x^n, x^n \in A^{n+1} \leftrightarrow \phi(x^n)</math>.
Definition of New Foundations; stratification
New Foundations (NF) is obtained from this theory by abandoning the distinctions of type. The axioms of this theory are extensionality (two objects with the same elements are the same object) and all those instances of comprehension obtained by dropping type indices (without introducing new identifications between variables) from an instance of comprehension of the streamlined type theory. It might seem that the resulting comprehension scheme would be the inconsistent scheme of naive set theory, but this is not the case: for example, the impossible Russell class <math>\{x \mid x \not\in x\}</math> is not constructed because there is no way to assign types consistently to all occurrences of x to obtain an instance of comprehension of the type theory.
It is traditional to describe the comprehension schema of NF in a way which makes no direct reference to types: a formula <math>\phi</math> is said to be stratified if there is a function f from variables (considered as pieces of syntax) to 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). The comprehension scheme for NF is the schema
- <math>\{x \mid \phi \}</math> exists
for each stratified formula <math>\phi</math>. Even the indirect reference to types in the notion of stratification can be eliminated: NF comprehension is equivalent to a finite conjunction of its instances, so NF can be finitely axiomatized without any reference to types at all.
Large sets appear
It is notable that NF (and the theory NFU + Infinity + Choice described below, which is known to be consistent) allow the construction of "big" sets. For example, <math>x=x</math> is a stratified formula, so the universal set V = <math>\{x \mid x=x\}</math> exists by stratified comprehension. In NF (as in the streamlined theory of types) the natural way to define natural numbers is Frege's: define each natural number n as the set of all sets with n elements (this can be done without the circularity of this summary). In general, a cardinal number is an equivalence class of sets under the relation <math>A \sim B</math> defined as "there is a bijection between A and B" and an ordinal number is an equivalence class of well-orderings under similarity. These definitions cannot be used in Zermelo set theory or its extensions because these classes are "too large".
The consistency problem and related partial results
The outstanding problem with this theory is the problem as to whether it is consistent. It is known that NF disproves Choice, and so proves Infinity (Specker, 1953). But it is also known (Jensen, 1969) that the minor(?) modification of allowing urelements (objects which have no elements but which are distinct from the empty set and from one another) produces a theory NFU which is known to be consistent (weaker than arithmetic) and consistent with Infinity and Choice as well. (This corresponds to a type theory TSTU in which positive types may contain urelements.) Some other variations are known to be consistent.
Specker has shown that NF is equiconsistent with TST + Amb, where Amb is the axiom scheme of typical ambiguity which asserts <math>\phi \leftrightarrow \phi^+</math> for any formula <math>\phi</math>, <math>\phi^+</math> being the formula obtained by raising every type index in <math>\phi</math> by one, and also 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 (and which cannot be used in instances of comprehension: it is external to the theory). The same results hold for various fragments of TST in relation to corresponding fragments of NF.
In the same year (1969) that Jensen showed consistency of NFU, Grishin showed the consistency of <math>NF_3</math>, the fragment of NF with full extensionality (no urelements) and those instances of the comprehension axiom which can be stratified using just three types. This theory is a very awkward medium for mathematics (though some efforts have been made to investigate ways to do things in this environment) largely because there is no obvious definition for an ordered pair. In spite of this awkwardness, <math>NF_3</math> is very interesting, because every infinite model of TST restricted to three types satisfies the ambiguity scheme of the previous paragraph, and so for every such model there is a model of <math>NF_3</math> with the same theory. This is already false for four types: <math>NF_4</math> is the same theory as NF, and we have no idea how to get an ambiguous model of TST with four types.
In 1983, Marcel Crabbé showed the consistency of the system NFI with unrestricted extensionality and those instances of the stratified comprehension axiom 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 (which is 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é notes in this connection the subtheory NFP of NFI in which only parameters (free variables) are allowed to have the type of the set asserted to exist by an instance of the comprehension axiom; this is called "predicative NF", though of course it is doubtful whether any theory with a self-membered universe is truly predicative. Randall Holmes has shown that NFP has the same consistency strength as the predicative theory of types of Bertrand Russell's Principia Mathematica without the Axiom of Reducibility.
Resolving the paradoxes in NF(U)
We review the paradoxes of set theory and their resolution in NF, noting that although the consistency of NF remains an open question, these solutions to the paradoxes can be seen to work in NFU, which is known to be consistent.
Relations and functions are defined in NF or NFU as sets of ordered pairs in the usual way. The Kuratowski ordered pair can be defined in this theory, but has the disadvantage that it is two types higher than its projections in TST, which means that a function is three types higher than the elements of its domain and range for purposes of stratification. If one can define a pair the same type as its arguments, then relations and functions are just one type higher than the elements of their domains and ranges. Such a pair is definable in NF (see the pair attributed to Rosser and Quine in the article on ordered pairs), the existence of such a 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). NFU + Infinity + Choice proves the existence of a type level ordered pair. The choice of pair only occasionally makes a difference here.
The Russell paradox is easy: <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 comprehension axiom of NF.
Cantor's paradox of the largest cardinal number exploits the application of Cantor's theorem to the universal set. Cantor's theorem says (in the usual set theory) 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>). Now of course there is an injection from <math>P(V)</math> into <math>V</math>, if <math>V</math> is the universal set! The resolution requires that we observe that <math>|A| < |P(A)|</math> makes no sense in the theory of types: the type of <math>P(A)</math> is one higher than the type of <math>A</math>. The correctly typed version (which is a theorem in the theory of types for essentially the same reasons that the original form of Cantor's theorem works in the usual set theory) is <math>|P_1(A)| < |P(A)|</math>, where <math>P_1(A)</math> is the set of one-element subsets of <math>A</math>. The specific instance of this theorem that interests us is <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; there is no reason to expect it to be a set, since its definition is unstratified. It is interesting to note that in all known models of NFU we have <math>|P_1(V)| < |P(V)| << |V|</math>; the Axiom of 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>.
We introduce some useful notions peculiar to this kind of set theory. 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 <math>A</math>, is a set is clearly cantorian and is said to be strongly cantorian.
The Burali-Forti paradox of the largest ordinal number goes as follows: we define (in naive set theory as in NF(U)) the ordinals as equivalence classes of well-orderings under similarity. There is an obvious natural well-ordering on the ordinals; since it is a well-ordering it belongs to an ordinal <math>\Omega</math>. It is straightforward to prove (by transfinite induction) that the order type of the natural order on the ordinals less than a given ordinal <math>\alpha</math> is <math>\alpha</math> itself. But this means that <math>\Omega</math> is the order type of the ordinals <math> < \Omega </math> and so is strictly less than the order type of all the ordinals -- but the latter is <math>\Omega</math> itself by definition! 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 <math>\alpha</math> is of a higher type than <math>\alpha</math>: if a type level ordered pair is used, it is 2 types higher, and if the usual Kuratowski ordered pair is used it is 4 types higher. For any order type <math>\alpha</math> we can define an order type <math>\alpha</math> one type higher: 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>. The T operation seems trivial but we will see that it is not. It is easy to show that it is a strictly monotone operation on the ordinals (it preserves order). Now we can restate the lemma on order types 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 pair is used (we assume the type level pair hereinafter). From this we deduce that the order type on the ordinals <math> <\Omega </math> is <math>T^2(\Omega)</math>, from which we deduce <math>T^2(\Omega)<\Omega</math>. This shows that the T operation is not a function (we cannot have a strictly monotone set map from ordinals to ordinals which sends an ordinal downward!). Since T is monotone, we have <math>\Omega > T^2(\Omega) > T^4(\Omega)\ldots</math>, a "descending sequence" in the ordinals which cannot be a set. 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 believe that the universe is a model of NFU, in spite of the fact that it is a set, because the membership relation is not a set relation.
For further development of mathematics in NFU, compared with the development in ZFC, look at the article implementation of mathematics in set theory.
Models of NFU
Here we discuss 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 <math>V_{\alpha}</math> of the cumulative hierarchy of sets. We may suppose without loss of generality that <math>j(\alpha)<\alpha</math>. 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 <math>V_{\alpha}</math>. The membership relation of the model of NFU will be
- <math>x \in_{NFU} y \equiv_{def} j(x) \in y \wedge y \in V_{j(\alpha)+1}</math>.
We prove that this actually is a model of NFU. Let <math>\phi</math> be a stratified formula in the language of NFU. Choose an assignment of types to all variables in the formula which witnesses the fact that it is stratified. Choose a natural number N greater than all types assigned to variables by this stratification.
Expand the formula <math>\phi</math> into a formula <math>\phi_1</math> in the language of the nonstandard model of Zermelo set theory with automorphism j using the definition of membership in the model of NFU. Application of any power of j to both sides of an equation or membership statement preserves its truth value because j is an automorphism. Make such an application to each atomic formula in <math>\phi_1</math> in such a way that each variable x assigned type i occurs with exactly <math>N-i</math> applications of j. The form of the atomic membership statements derived from the NFU membership and the fact that the formula is stratified make this possible. Each quantified sentence <math>(\forall x \in V_{\alpha}.\psi(j^{N-i}(x)))</math> can be converted to the form <math>(\forall x \in j^{N-i}(V_{\alpha}).\psi(x))</math> (and similarly for existential quantifiers). Carry out this transformation everywhere to obtain a formula <math>\phi_2</math> in which j is nowhere applied to a bound variable.
Choose any free variable y in <math>\phi</math> assigned type i. Apply <math>j^{i-N}</math> uniformly to the entire formula to obtain a formula <math>\phi_3</math> in which y appears without any application of j. Now <math>\{y \in V_{\alpha} \mid \phi_3\}</math> exists (because j appears applied only to free variables and constants), belongs to <math>V_{\alpha+1}</math>, and contains exactly those y which satisfy the original formula <math>\phi</math> in the model of NFU. <math>j(\{y \in V_{\alpha} \mid \phi_3\})</math> has this extension in the model of NFU (the application of j corrects for the different definition of membership in the model of NFU). This establishes that Stratified Comprehension holds in the model of NFU.
To see that weak extensionality holds is straightforward: each nonempty element of <math>V_{j(\alpha)+1}</math> inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.
The basic idea is that the "power set" <math>V_{\alpha+1}</math> of our "universe" <math>V_{\alpha}</math> is coded via the automorphism j into its externally isomorphic copy <math>V_{j(\alpha)+1}</math> inside our "universe", and the remaining objects not coding subsets of the universe are treated as urelements.
If <math>\alpha</math> is a natural number n, we get a model of NFU which claims that the universe is finite (it is externally infinite, of course). If <math>\alpha</math> is infinite and the Axiom of Choice holds in the nonstandard model of Zermelo set theory, we obtain 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 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 <math>T_i</math> (all of the same type in the metatheory) with embeddings of each <math>P(T_i)</math> into <math>P_1(T_{i+1})</math> coding embeddings of the power set of <math>T_i</math> into
<math>T_{i+1}</math> in a type-respecting manner). Given an embedding of <math>T_0</math> into <math>T_1</math> (identifying elements of the base "type" with subsets of the base type), one can define embeddings from each "type" into its successor in a natural way. This can be generalized to transfinite sequences <math>T_{\alpha}</math> with care. Note that the construction of such sequences of sets is limited by the size of the type in which they are being constructed; this prevents TSTU from proving its own consistency (TSTU + Infinity can prove the consistency of TSTU; to prove the consistency of TSTU+Infinity one needs a type containing a set of cardinality <math>\beth_{\omega}</math>, which cannot be proved to exist in TSTU+Infinity without stronger assumptions). Now the same results of model theory can be used to build a model of NFU and verify that it is a model of NFU in much the same way, with the <math>T_{\alpha}</math>'s being used in place of <math>V_{\alpha}</math> in the usual construction. The final move is to observe that since NFU is consistent, we can drop the use of absolute types in our metatheory, bootstrapping the metatheory from TSTU to NFU.
Facts about the automorphism j
The automorphism j of a model of this kind is closely related to certain natural operations in NFU. For example, if <math>W</math> 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 model construction) and W has type <math>\alpha</math> in NFU, then <math>j(W)</math> will be a well-ordering of type <math>T(\alpha)</math> in NFU.
In fact, j is coded by a function in the model of NFU. The function in the nonstandard model which sends the singleton of any element of <math>V_{j(\alpha)}</math> to its sole element becomes a function in NFU which sends each singleton <math>\{x\}</math> for x any object in the universe to <math>j(x)</math>. If we call this function Endo, it has the following properties: Endo is an injection from the set of singletons into the set of sets with the property that <math>Endo(\{x\}) = \{Endo(\{y\}) \mid y \in x\}</math> for each set x. This function can be used to define a type level "membership" relation on the universe which reproduces the membership relation of the original nonstandard model.
Strong Principles
In this section we usually consider NFU, which is known to be consistent, and discuss the effect of various "strong axioms of infinity".
One can add such axioms as "there is an inaccessible cardinal" to NFU, but it is more natural to consider principles appropriate to this theory, usually assertions about cantorian and strongly cantorian sets: these are ways to strengthen the theory in its own terms, and they have the effect of causing large cardinals of the usual sorts to appear.
NFU + Infinity + Choice, our usual base theory, has the same strength as TST + Infinity or Zermelo set theory with separation restricted to bounded formulas.
The weakest of the usual strong principles is the following:
- Rosser's Axiom of Counting The set of natural numbers is a strongly cantorian set.
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 <math>\{m \mid 1 \leq m \leq n\}</math> has n members", for each natural number n". This intuitively obvious assertion is unstratified: what is provable in NFU is "the set <math>\{m \mid 1 \leq m \leq n\}</math> has <math>T^2(n)</math> members" (where the T operation on cardinals is defined by <math>T(|A|) = |P_1(A)|</math>; this raises the type of a cardinal by one). For any cardinal number (including natural numbers) to assert <math>T(|A|) = |A|</math> is equivalent to asserting that the sets A of that cardinality are cantorian (by a usual abuse, we refer to such cardinals as "cantorian cardinals"). 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.
The Axiom of 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 <math>\beth_n</math> exists, but not that <math>\beth_{\omega}</math> exists; NFU + Counting proves Infinity (this is easy) and further proves the existence of <math>\beth_{\beth_n}</math> for each n, but not the existence of <math>\beth_{\beth_{\omega}}</math>. (See article on beth numbers).
The Axiom of Counting implies immediately that one does not need to assign types to variables restricted to the set <math>N</math> 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 the Axiom of Counting is less important in practice than the convenience of not having to annotate variables known to have natural number values (or related kinds of values) with singleton brackets or applications of the T operation in order to get stratified set definitions.
The Axiom of Counting implies Infinity; each of the axioms below needs to be adjoined to NFU + Infinity to get the effect of strong axioms 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 the Axiom of 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
- Axiom of strongly cantorian separation: For any strongly cantorian set A and any formula <math>\phi</math> (not necessarily stratified!) the set <math>\{x \in A \mid \phi\}</math> exists.
Immediate consequences of this 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 + <math>\Sigma_2</math> Replacement.
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 is a sufficient condition, not a necessary one.
Next is
- Axiom of Cantorian Sets: Every cantorian set is strongly cantorian.
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 + the scheme 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 Zermelo theory are an initial (proper class) segment of the ordinals of the model.
Next consider the
- Axiom of Cantorian Separation: For any cantorian set A and any formula <math>\phi</math> (not necessarily stratified!) the set <math>\{x \in A \mid \phi\}</math> exists.
This combines the effect of the two preceding axioms and is actually even stronger (we do not know exactly how strong). There is a proof by unstratified mathematical induction that there are n-Mahlo cardinals for every n, given the Axiom of Cantorian Sets, which gives an extension of ZFC which 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 Zermelo set theory. This is again a sufficient but not a necessary condition.
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 the Axiom of Cantorian Sets is the
- Axiom of Large Ordinals: For each noncantorian ordinal <math>\alpha</math>, there is a natural number n such that <math>T^n(\Omega) < \alpha</math>.
Recall that <math>\Omega</math> is the order type of the natural order on all ordinals. This only implies Cantorian Sets if we have Choice (but is at that level of consistency strength in any case). It is remarkable that one can even define <math>T^n(\Omega)</math>: this is the nth term <math>s_n</math> of any finite sequence of ordinals s of length n such that <math>s_0 = \Omega</math>, <math>s_{i+1} = T(s_i)</math> for each appropriate i. Note that this is a completely unstratified definition. The uniqueness of <math>T^n(\Omega)</math> can be proved (for those n for which it exists) and a certain amount of common-sense reasoning about this notion can be carried out; enough to show that the Axiom 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 <math>j^{-i}(\alpha)</math> in the underlying nonstandard model of Zermelo set theory.
- Axiom of Small Ordinals: For any formula <math>\phi</math>, 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>.
Solovay has shown the precise equivalence in consistency strength of NFUB = NFU + Infinity + Cantorian Sets + Small Ordinals with Kelley-Morse 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! The theory NFUB- which omits Cantorian Sets from the above is easily seen to have the same strength.
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 Zermelo set theory.
Even stronger is the theory NFUM = NFU + Infinity + Large Ordinals + Small Ordinals. This is equivalent to Kelley-Morse set theory with a predicate on the classes which is a <math>\kappa</math>-complete nonprincipal ultrafilter on the proper class ordinal <math>\kappa</math>; in effect, this is Kelley-Morse set theory + "the proper class ordinal is a measurable cardinal"!
The technical details here are not the main point. The point is that seemingly reasonable assertions which suggest themselves naturally in the context of NFU turn out to be equivalent in power to very strong axioms of infinity in the ZFC context. A reason for this is seen in the correlation between the existence of models of NFU of the kind described above which satisfy these axioms and the existence of models of Zermelo set theory with automorphisms with special properties.
See also
- Axiomatic set theory
- Positive set theory
- Alternative set theory
- Implementation of mathematics in set theory
External links
- Bibliography of Set Theory with a Universal Set
- New Foundations Home Page
- Elementary Set Theory with a Universal Set This is the online version of Randall Holmes's elementary set theory text in NFU. Holmes has permission from the publishers to provide access to this on the web.