Past exam of the mathematics course of the University of Cambridge / 2005 / iii / Paper 27 / 9

We give a relative consistency proof: a model of ZFC yields a model of NFU. This proves the requested consistency relative to the usual background set theory; it does not claim the optimal, much weaker consistency bound for bare NFU.

Recall that New Foundations with urelements has a unary set predicate $S$, atoms without members, extensionality restricted to sets, and comprehension for every stratified formula. Stratification assigns integer types to variables, with equal types at equality and adjacent types at membership. We construct a model of simple typed set theory with atoms with a type-shifting automorphism, then identify its types using that automorphism.

Start with a model of ZFC and a Skolem expansion of it. By the compactness theorem there is a model $N$ of the same expanded theory with an increasing integer-indexed order-indiscernible sequence of ordinals $⟨c_i:i\in \mathbb{Z}⟩$, all above $\omega$. Here is the finite-satisfiability argument. A finite fragment names only finitely many $c_i$ and asks for equal truth values of finitely many formulas on increasing tuples. In the starting model choose an infinite increasing sequence of ordinals above $\omega$. Colour its finite subsets by these truth vectors, successively treating each tuple length. The Ramsey's theorem supplies an infinite homogeneous subsequence for the finitely many colours and arities. Its first required number of elements interprets all named $c_i$ and satisfies that fragment. Compactness gives the entire sequence. This argument works for the countable expanded language because each fragment uses only finitely many formulas.

Replace $N$ by the Skolem hull of the $c_i$. The mapis well defined by indiscernibility: equal terms remain equal after shifting their increasing lists of indices. The same argument preserves every formula. Shifting indices backwards gives its inverse, so $j$ is an automorphism of the hull, and $j(c_i)=c_{i+1}>c_i$. The Skolem hull is elementary by its witness functions. This is a concrete Ehrenfeucht-Mostowski model; it is not an elementary class self-embedding of the actual well-founded universe.

Set $D_i=V_{c_i}^N$, interpreted externally as the objects belonging to that internal rank segment, for every integer $i$. At type $i$ declareand define adjacent-type membership byThe members of a type-$i+1$ set are exactly a subset of $D_i$; a type-$i+1$ atom has no ${\epsilon }_i$-members. Every internal subset of $D_i$ is an object of $D_{i+1}$, since $c_{i+1}>c_i$. Extensionality for sets is inherited from $N$. For a typed formula involving finitely many types, restrict its quantifiers to the corresponding internal $D_k$ and express each $S_k$ and ${\epsilon }_k$ by the displayed definitions. Separation in $N$ gives the required subset of $D_i$, which represents its comprehension at type $i+1$. This verifies the typed theory even though many higher-type objects are atoms. The automorphism $j$ carries $D_i,S_i,{\epsilon }_i$ to the next type.

On domain $D_0$, define $S(x)=S_0(x)$ andIf $S(y)$ is false, $S_1(j(y))$ is false, so $y$ has no $E$-members. For sets $y,z$, equality of their $E$-extensions gives equality of the typed sets $j(y),j(z)$ and hence $y=z$. To check stratified comprehension, translate a variable of type $k$ into $j^k(x)$. The automorphism laws make membership and equality translate exactly. A stratified predicate on a variable of type zero defines a typed subset $B$ of $D_0$, represented by a set at type one. Then $b=j^{-1}(B)\in D_0$ has $E$-extension exactly that predicate. A uniform type shift handles any other type assigned to the comprehended variable. The resulting untyped structure is a model of NFU.