= Solution
A <definable continuous hierarchy> is a definable class function $\alpha\mapsto H_\alpha$ on the <ordinals>, with set-valued levels, such that $H_\alpha\subseteq H_\beta$ for $\alpha<\beta$ and
$$
H_\lambda=\bigcup_{\alpha<\lambda}H_\alpha
$$
for nonzero <limit ordinals>. Its union is a definable <class in set theory> $H$. Often the definition additionally requires every level to be a <transitive set>; the following statement also works without that requirement.
The <reflection theorem for definable hierarchies> says that for any finite collection $\mathcal F$ of <first-order formulas>, there is a <closed unbounded> class of <ordinals> $\alpha$ such that, for every $\varphi\in\mathcal F$ and every parameter tuple from $H_\alpha$,
$$
\boxed{(H_\alpha,\in)\models\varphi(\vec a)\ \Longleftrightarrow\ (H,\in)\models\varphi(\vec a).}
$$
A useful justification is the witness-closure proof. Close $\mathcal F$ under subformulas. At each level and for each existential subformula, bound the least level containing a witness for each parameter tuple for which a witness exists in $H$. <Axiom schema of replacement> bounds these indices. Iterating the finitely many bounds through $\omega$ produces a limit level containing all required witnesses. Induction on the <first-order formulas>, equivalently the finite-formula version of the <Tarski-Vaught test>, yields agreement. Continuity gives closedness of the reflecting class, and starting above any prescribed <ordinal> gives unboundedness. This is finite reflection, not a claim that all <first-order formulas> reflect simultaneously in an arbitrary hierarchy.
Back to article page
