Set-theoretic absoluteness

A formula is absolute between transitive classes $M\subseteq N$ when it has the same truth value in both structures for parameters from $M$.

A formula is upward absolute when its truth in a smaller transitive class implies its truth in a larger one. Existential formulas with bounded matrices are upward absolute because their witnesses remain available.

A formula is downward absolute when its truth in a larger transitive class implies its truth in a smaller one. Universal formulas with bounded matrices are downward absolute.

The Lévy hierarchy classifies formulas of set theory by their alternations of unbounded quantifiers, ignoring bounded quantifiers of the forms $\forall x\in y$ and $\exists x\in y$.

A formula is ${\Delta }_1^{\mathrm{ZF}}$ when ZF proves it equivalent both to a ${\Sigma }_1$ formula and to a ${\Pi }_1$ formula. Such formulas are absolute between suitable transitive models of finite fragments of ZF.