= Rank-shifting NFU model with explicit set predicate
{title2=$S(y)\iff j(y)\subseteq D,\quad x\mathrel E y\iff S(y)\land x\in j(y)$}
Let $M$ be a membership structure satisfying <extensionality> and every pure-membership separation instance, with an external automorphism $j$ and domains $D_i=j^i(D_0)$ represented by objects of $M$. Suppose every $M$-subset of $D_i$ is an element of $D_{i+1}$. Interpret <NFU> on the objects of $D_0$ using the displayed <set> predicate and membership, with all <subset> statements evaluated in $M$. Atoms have no members, and <extensionality> applied to $j(y),j(z)\subseteq D_0$ gives <extensionality> for <sets>. A <stratified formula> becomes an ordinary pure-membership formula by sending each variable of type $i$ to $j^i(x)$ and restricting its quantifier to $D_i$. A <set> predicate on sort $i$ means containment in $D_{i-1}$; adjacent-sort membership is guarded by containment in the lower domain. Separation yields the extension $X\subseteq D_i$, the closure hypothesis places it in $D_{i+1}$, and $j^{-(i+1)}(X)\in D_0$ is the required untyped <set>. This proves every comprehension instance. The guard is essential: an object not contained in a lower domain can still have some ordinary members there, which must not become members of a typed atom. Internal ranks $V_{j^i(\alpha)}$ with $j(\alpha)>\alpha$ give one instance of these hypotheses; shifted rank objects in an elementary model of an expanded $V_{\omega+\omega}$ give a consistency proof without assuming Con(<ZFC>).
Back to article page
