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 **NF with urelements** (**NFU**), an important variant of NF due to Jensen^{[1]} and clarified by Holmes.^{[2]} In 1940 and in a revision in 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.^{[3]} That is to say, it is an axiomatic set theory that allows infinite descending chains of membership, such as
… x_{n} ∈ x_{n-1} ∈ … ∈ x_{2} ∈ x_{1}. 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.

New Foundations is closely related to **Russellian unramified typed set theory** (**TST**), a streamlined version of the theory of types of *Principia Mathematica* with a linear hierarchy of types.

The primitive predicates of TST are equality () and membership (). TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each (meta-) 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.

When writing formulas in a many-sorted theory such as TST, some annotations are usually added to variables to denote their types. In TST it is customary to write the *type indices* as superscripts: denotes a variable of type *n*. Thus the following two atomic formulas succinctly describe the typing rules: and . (Quinean set theory seeks to eliminate the need to write out these type indices explicitly.)

The axioms of TST are:

- Extensionality: sets of the same (positive) type with the same members are equal;
- An axiom schema of comprehension, namely:

- If is a formula, then the set exists.

- In other words, given any formula , the formula is an axiom where represents the set and is not free in .

This type theory is much less complicated than the one first set out in the *Principia Mathematica*, which included types for relations whose arguments were not necessarily all of the same types. 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.

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 is said to be stratified if there exists a function *f* from pieces of 's syntax to the natural numbers, such that for any atomic subformula of we have *f*(*y*) = *f*(*x*) + 1, while for any atomic subformula of , we have *f*(*x*) = *f*(*y*). *Comprehension* then becomes:

- exists for each stratified formula .

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

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 , 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 and , i.e., functions such that and (in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of for any stratified formula is considered a theorem and only proved later, so expressions like 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 , and the successor operation can be defined in a stratified way:

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 would be an inductive set.

Since inductive sets always exist, the set of natural numbers can be defined as the intersection of all inductive sets. This definition enables mathematical induction for stratified statements , because the set can be constructed, and when satisfies the conditions for mathematical induction, this set is a inductive set.

Finite sets can then be defined as sets that belong to a natural number. However, it is not trivial to prove that is not a "finite set", i.e., that the size of the universe is not a natural number. Suppose that . Then (it can be shown inductively that a finite set is not equinumerous with any of its proper subset), , and each subsequent natural number would be too, causing arithmetic to break down. To prevent this, one can introduce the **axiom of infinity** for NF:

^{[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 . 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 is a non-standard natural number. In such models, mathematical induction can prove statements about , making it impossible to "distinguish" 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 is infinite. - In NFU with axioms asserting the existence of a type-level ordered pair, is equinumerous with its proper subset , which implies
*Infinity*.^{[7]}Conversely, NFU +*Infinity*+*Choice*proves the existence of a type-level ordered pair.^{[citation needed]}NFU +*Infinity*interprets NFU + "there is a type-level ordered pair" (they are not quite the same theory, but the differences are inessential).^{[citation needed]}

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

Of course there is an injection from into since 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 . In NF, and should be assigned the same type, so the definition of is not stratified. Indeed, if is the trivial injection , then is the same (ill-defined) set in Russell's paradox.

This failure is not surprising since makes no sense in TST: the type of is one higher than the type of . In NF, 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 with , the set of one-element subsets of . Indeed, the correctly typed version of Cantor's theorem is a theorem in TST (thanks to the diagonalization argument), and thus also a theorem in NF. In particular, : 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 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 .

However, unlike in TST, is a syntactical sentence in NF(U), and as shown above one can talk about its truth value for specific values of (e.g. when it is false). 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**.^{[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 that corresponds to the natural well-ordering of all ordinals, but that does not mean that 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 can be defined with no problem. Transfinite induction works on stratified statements, which allows one to prove that the natural ordering of ordinals ( iff there exists well-orderings such that is a continuation of ) is an well-ordering of . By definition of ordinals, this well-ordering also belongs to an ordinal . In naive set theory, one would go on to prove by transfinite induction that each ordinal is the order type of the natural order on the ordinals less than , which would imply an contradiction since by definition is the order type of *all* ordinals, not any proper initial segment of them.

However, the statement " is the order type of the natural order on the ordinals less than " is not stratified, so the transfinite induction argument does not work in NF. In fact, "the order type of the natural order on the ordinals less than " is at least *two* types higher than : The order relation is one type higher than assuming that is a type-level ordered pair, and the order type (equivalence class) is one type higher than . If is the usual Kuratowski ordered pair (two types higher than and ), then would be *four* types higher than .

To correct such a type problem, one needs the **T operation**, , that "raises the type" of an ordinal , just like how "raises the type" of the set . The T operation is defined as follows: If , then is the order type of the order . 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 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 is always less than , the order type of *all* ordinals. In particular, .

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., iff . Hence the T operation is not a function: The collection of ordinals cannot have a least member, and thus cannot be a set. More concretely, the monotonicity of T implies , 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 is a model of NFU, despite 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.

Where the starting point for the metamathematics of Zermelo-Fraenkel set theory is the easy-to-formalize intuition of the cumulative hierarchy, the non-well-foundedness of NF and NFU makes this intuition not directly applicable. However, the intuition of forming sets at a stage from sets developed at earlier stages can be augmented to allow forming sets at a stage consisting of all possible sets but given sets formed at earlier stages, giving an analogous iterative conception of set.^{[12]}^{[specify]}

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 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 (and similarly for existential quantifiers). 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 (because *j* appears applied only to free variables and constants), 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 (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 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 (it is externally infinite, of course). If is infinite and the *Choice* holds in the nonstandard model of ZFC, one obtains a model of NFU + *Infinity* + *Choice*.

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 (all of the same type in the metatheory) with embeddings of each into coding embeddings of the power set of into in a type-respecting manner). Given an embedding of into (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 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 , 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 '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.

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

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

**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 {*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 members" (where the *T* operation on cardinals is defined by ; this raises the type of a cardinal by one). For any cardinal number (including natural numbers) to assert is equivalent to asserting that the sets *A* of that cardinality are Cantorian (by a usual abuse of language, 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.

*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* (easily) proves *Infinity*, and further proves the existence of for each n, but not the existence of . (See beth numbers).

*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 (or related kinds of 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

**Axiom of strongly Cantorian separation**: For any strongly Cantorian set*A*and any formula (not necessarily stratified!) the set exists.

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 + *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 condition is sufficient but not necessary.

Next is

**Axiom of Cantorian Sets**: Every Cantorian set is strongly Cantorian.

This very simple 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

**Axiom of Cantorian Separation**: For any Cantorian set A and any formula (not necessarily stratified!) the set {*x*∈*A*|φ} exists.

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

**Axiom of Large Ordinals**: For each non-Cantorian ordinal , there is a natural number*n*such that .

Recall that 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 : this is the *n*th 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 (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 *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.

**Axiom of Small Ordinals**: For any formula φ, there is a set*A*such that the elements of*A*which are strongly Cantorian ordinals are exactly the strongly Cantorian ordinals such that φ.

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 non-principal 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.

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 J. Barkley Rosser^{[13]} proved that the system presented in *Mathematical Logic* was subject to the Burali-Forti paradox. This result does not apply to NF. Hao Wang^{[14]} 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 consistency of the revised ML implies the consistency of NF. That is, NF and the revised ML are equiconsistent.