Stratified formula

A formula is stratified if its variables can be assigned integer types so that equality relates variables of the same type and membership $x\in y$ requires $\mathrm{type}(y)=\mathrm{type}(x)+1$. Unary set predicates impose no additional difference. Stratification is a syntactic condition; it does not assert that the untyped universe actually has disjoint types. Translating a stratified formula into a typed model permits type-shifting automorphism to recover untyped comprehension.