= Rank-indiscernible construction of an NFU model
<NFU> has a unary predicate $S$ for <sets>, atoms have no members, <extensionality> applies to <sets>, and comprehension applies to every <stratified formula>. A stratification assigns integer types to variables so that equality uses equal types and $x\in y$ requires $\operatorname{type}(y)=\operatorname{type}(x)+1$. A unary <set> predicate adds no type difference.
Start with the actual <set> structure $B=(V_{\omega+\omega},\in)$. This structure satisfies <extensionality> and every pure-membership <separation> instance: the <subset> defined in a <set> $a$ of rank below $\omega+\omega$ still has rank below $\omega+\omega$. We do not assert that $B$ satisfies <replacement> or all of <ZFC>. Expand it by <Skolem functions>. In it use the <sequence> of rank objects $V_{\omega+n+6}$, $n<\omega$. For two such objects $d<e$ in <sequence> order, we have
$$
d\subsetneq e,\qquad \forall x\,(x\subseteq d\Longrightarrow x\in e),
$$
with quantifiers in $B$. The second statement holds because every <subset> of $V_\alpha$ belongs to $V_{\alpha+1}$, and the later rank is at least $\alpha+1$.
Introduce constants $d_i$, $i\in\mathbb Z$, and require them to be order indiscernibles in the Skolem language, satisfying these two assertions whenever $i<j$. Also require $V_{\omega+5}\subseteq d_i$ for every $i$; this fixed rank object is first-order definable in $B$. Every finite part of these requirements together with $\operatorname{Th}(B^*)$ is satisfiable: color finite increasing tuples of the original rank <sequence> by the truth values of the finitely many formulas mentioned, and use <Ramsey's theorem> to get a homogeneous <subsequence>. The rank assertions hold for every increasing tuple there. The <compactness theorem> gives a model of the full theory. In its <Skolem hull> $N$ generated by the $d_i$, the integer shift extends to an <automorphism> $j$ with $j(d_i)=d_{i+1}$, by the term-transport proof of the <Ehrenfeucht-Mostowski theorem>. Thus $N$ still satisfies <extensionality> and all pure-membership <separation> instances, and
$$
N\models\forall x\,(x\subseteq d_i\Longrightarrow x\in d_{i+1})
\quad(i\in\mathbb Z).
$$
This is a set-sized <first-order model>; no satisfaction predicate for a proper-class universe is being assumed.
Externally let $D_i=\{x\in N:N\models x\in d_i\}$. The <automorphism> bijects $D_i$ onto $D_{i+1}$. Interpret a typed structure with sort $i$ equal to $D_i$. At sort $i+1$, declare $y$ a <set> exactly when $N\models y\subseteq d_i$; otherwise it is an atom. Define adjacent-sort membership by
$$
x\in_i y\quad\Longleftrightarrow\quad N\models(y\subseteq d_i\ \land\ x\in y).
$$
The guard is necessary: a typed atom might have some ordinary $N$-members in $D_i$, and those must not become its typed members. Set-extensionality follows from <extensionality> in $N$, because the ordinary members of a typed <set> all lie in $D_i$. For any typed formula on sort $i$, its quantifiers can be restricted to the corresponding $d_l$, its <set> predicates replaced by <subset> assertions, and its memberships replaced by the guarded relation. This is an ordinary pure-membership formula of $N$ with finitely many parameters. <Separation> gives its extension $X\subseteq d_i$, and the displayed closure assertion gives $X\in d_{i+1}$. It is therefore a typed <set> witnessing comprehension. The <automorphism> shifts these sorted domains and preserves the <set> flags and guarded memberships.
Collapse the types onto $D_0$. Define
$$
S(y)\quad\Longleftrightarrow\quad N\models j(y)\subseteq d_0,
\qquad x\mathrel E y\quad\Longleftrightarrow\quad S(y)\ \land\ N\models x\in j(y).
$$
Objects not satisfying $S$ have no $E$-members. If two <sets> have the same $E$-members, their images under $j$ are <subsets> of $d_0$ with the same ordinary members, so are equal by <extensionality> of $N$; injectivity of $j$ gives equality of the original objects.
To verify every stratified comprehension instance, assign a variable $v$ its stratification type $t(v)$ and translate its value $a\in D_0$ to $j^{t(v)}(a)\in D_{t(v)}$. Equality is preserved. An atomic $E(x,y)$ translates to the guarded adjacent-sort membership because $t(y)=t(x)+1$; the unary predicate $S(y)$ translates to $j^{t(y)}(y)\subseteq d_{t(y)-1}$. <Induction> on formulas, using the domain bijections for quantifiers, preserves truth. If the free variable $x$ has type $t$, typed comprehension produces its extension $X\subseteq d_t$, with $X\in d_{t+1}$. Put $b=j^{-(t+1)}(X)\in D_0$. Then $S(b)$ holds, and for every $a\in D_0$,
$$
a\mathrel E b\quad\Longleftrightarrow\quad N\models j^t(a)\in X
\quad\Longleftrightarrow\quad \varphi(a,\vec p).
$$
This is exactly the required <NFU> <set>. No formula containing the external <automorphism> $j$ has been used in a <separation> or comprehension scheme; $j$ only transports values after the pure formula is formed.
The construction also permits the usual <infinity> requirement. The ordinary $\omega$ and its successor graph $f$ are definable in $N$, hence fixed by $j$, and lie below $V_{\omega+5}$, so belong to all the required domains. Under $E$, the members of $\omega$ are still its ordinary $N$-members. The new Kuratowski pair satisfies
$$
\langle x,y\rangle_E=j^{-2}(\langle x,y\rangle_N).
$$
Since $j(f)=f$, membership of this pair in $f$ under $E$ is equivalent to $\langle x,y\rangle_N\in f$. Thus $f$ is an internal injection of $\omega$ into itself omitting zero, giving a Dedekind-infinite <set>.
We have built a model of <NFU>, with <infinity> if it is included in the formulation, in ordinary <ZFC> metatheory:
$$
\boxed{\text{ZFC proves the existence of a model of NFU.}}
$$
In particular $\operatorname{Con}(\mathrm{ZFC})\Rightarrow\operatorname{Con}(\mathrm{NFU})$. This proof does not assume $\operatorname{Con}(\mathrm{ZFC})$ as an additional internal axiom: its starting structure is the <set> $V_{\omega+\omega}$, not a model of <ZFC>.
Back to article page
