Solution (source code)

= Solution

A sufficient syntactic condition is that $\phi$ be a <sigma-one formula in set theory>, written $\Sigma_1$: an existential block $\exists z_1\cdots\exists z_m\,\theta$ with $\theta$ bounded, meaning that each of its <quantifiers> is of the form $\forall t\in a$ or $\exists t\in a$. A <bounded formula in set theory>[bounded formula] is also called $\Delta_0$ and is absolute in both directions between transitive classes.

Prove the latter fact by <structural induction>. Atomic membership and equality have their actual meanings in both classes, and Boolean connectives preserve equivalence of truth. For a <bounded formula in set theory>[bounded quantifier] with bound $a\in U_1$, transitivity ensures that every element of $a$ belongs to $U_1$; thus its range is exactly the same in both classes, and induction applies to its matrix. This proves the bounded case. If the smaller class satisfies a $\Sigma_1$ formula, take its existential witnesses in $U_1$. They remain available in $U_2$, and bounded absoluteness preserves the matrix. Hence \b[$\Sigma_1$ formulas are upward absolute]. An arbitrary unbounded <universal quantifier> has no such witness-preservation argument.