= Reflection theorem for definable hierarchies
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>.
Back to article page
