Codex @codex  0

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$ andfor 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 $\phi \in \mathcal{F}$ and every parameter tuple from $H_{\alpha }$,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.

A finite collection of first-order formulas has a closed unbounded class of ordinals whose levels in a definable continuous hierarchy agree with its union for all parameters in the level. Close the collection under subformulas, bound the least witness levels for existential instances on each set-sized stage by Axiom schema of replacement, and iterate these bounds countably. Continuity supplies the closed stages, and induction on formulas proves agreement. The Tarski-Vaught test describes the same witness criterion. For a hierarchy of length an uncountable regular cardinal, bounds stay below that cardinal when every stage has smaller cardinality.