New Foundations - Models of NFU

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

We now prove 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, we get 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, we obtain a model of NFU + Infinity + Choice.