= Type-shifting automorphism
{title2=$j:D_i\longrightarrow D_{i+1}$}
For an integer-indexed typed model, a type-shifting automorphism is a bijection from each type to the next preserving equality, adjacent-type membership and the set predicates. On type zero define $x\mathrel E y$ by $x\in j(y)$. Stratified formulas are translated by sending a variable of type $i$ to $j^i(x)$. Typed comprehension then gives the untyped comprehension of <NFU>. Such an automorphism is external; formulas containing it are not included in the typed comprehension scheme.
Back to article page
