linguistic:translation, information:classification
Models of NFU

Jensen's proof gives 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 V α {\displaystyle V_{\alpha }} of the cumulative hierarchy of sets. We may suppose without loss of generality that j (α) < α {\displaystyle j(\alpha)<\alpha }.

The domain of the model of NFU will be the nonstandard rank V α {\displaystyle V_{\alpha }}. The basic idea is that the automorphism j codes the "power set" V α + 1 {\displaystyle V_{\alpha +1}} of our "universe" V α {\displaystyle V_{\alpha }} into its externally isomorphic copy V j (α) + 1 {\displaystyle V_{j(\alpha)+1}} inside our "universe." The remaining objects not coding subsets of the universe are treated as urelements. Formally, the membership relation of the model of NFU will be x ∈ N F U y ≡ d e f j (x) ∈ y ∧ y ∈ V j (α) + 1. {\displaystyle x\in _{NFU}y\equiv _{def}j(x)\in y\wedge y\in V_{j(\alpha)+1}.}

It may now be proved that this actually is a model of NFU. Let ϕ {\displaystyle \phi } 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 ϕ {\displaystyle \phi } into a formula ϕ 1 {\displaystyle \phi _{1}} 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 ϕ 1 {\displaystyle \phi _{1}} in such a way that each variable x assigned type i occurs with exactly N − i {\displaystyle N-i} 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 (∀ x ∈ V α. ψ (j N − i (x))) {\displaystyle (\forall x\in V_{\alpha }.\psi (j^{N-i}(x)))} can be converted to the form (∀ x ∈ j N − i (V α). ψ (x)) {\displaystyle (\forall x\in j^{N-i}(V_{\alpha }).\psi (x))} (and similarly for existential quantifiers). Carry out this transformation everywhere and obtain a formula ϕ 2 {\displaystyle \phi _{2}} in which j is never applied to a bound variable. Choose any free variable y in ϕ {\displaystyle \phi } assigned type i. Apply j i − N {\displaystyle j^{i-N}} uniformly to the entire formula to obtain a formula ϕ 3 {\displaystyle \phi _{3}} in which y appears without any application of j. Now { y ∈ V α ∣ ϕ 3 } {\displaystyle \{y\in V_{\alpha }\mid \phi _{3}\}} exists (because j appears applied only to free variables and constants), belongs to V α + 1 {\displaystyle V_{\alpha +1}}, and contains exactly those y which satisfy the original formula ϕ {\displaystyle \phi } in the model of NFU. j ({ y ∈ V α ∣ ϕ 3 }) {\displaystyle j(\{y\in V_{\alpha }\mid \phi _{3}\})} 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 V j (α) + 1 {\displaystyle V_{j(\alpha)+1}} inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.

If α {\displaystyle \alpha } 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 α {\displaystyle \alpha } is infinite and the Choice holds in the nonstandard model of ZFC, one obtains a model of NFU + Infinity + Choice.