= 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 $\operatorname{type}(y)=\operatorname{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.
Back to article page
