The Lévy hierarchy and absoluteness

In the pure membership language, ${\mathrm{\Delta }}_0$ consists of atomic formulas and their Boolean combinations and bounded quantifications $\mathrm{\exists }x\in a$ and $\mathrm{\forall }x\in a$ (the bound does not contain $x$). Put ${\mathrm{\Sigma }}_0={\mathrm{\Pi }}_0={\mathrm{\Delta }}_0$. Simultaneously, ${\mathrm{\Sigma }}_{n+1}$ is the closure of ${\mathrm{\Pi }}_n$ under unbounded existential quantification, finite conjunction/disjunction, and bounded quantification; ${\mathrm{\Pi }}_{n+1}$ is the dual closure of ${\mathrm{\Sigma }}_n$ under unbounded universal quantification, the positive Boolean operations, and bounded quantification. Empty conjunction and disjunction mean truth and falsity. Negation exchanges the two classes after De Morgan expansion.

A formula is $T$-${\mathrm{\Sigma }}_n$ if $T$ proves it equivalent to such a formula, and similarly for ${\mathrm{\Pi }}_n$; $T$-${\mathrm{\Delta }}_n$ means both. Unless specified otherwise the equivalence theory here is ZF. This is a hierarchy of set quantifiers, distinct from the arithmetic hierarchy.

For nonempty membership domains $M\subseteq N$, absoluteness of $\varphi$ means ${\varphi }^M(\bar{a})\leftrightarrow {\varphi }^N(\bar{a})$ for every tuple $\bar{a}\in M$ of its parameters. For definable classes this is a scheme, using relativization separately for each external formula.

The formula constructors and fresh-variable convention are those of Terms and formulas as finite set codes. Expand bounded quantifiers before applying Relativization to sets and definable classes. No satisfaction predicate for the universe is being defined. Compare Marks, Definition 18.8 and Exercise 18.9, printed p.76: bounded closure is built into our syntax; its existential normal form needs a separate ZF argument.