Use a definable cumulative hierarchy of set-sized stages: for , at nonzero limits, and . Class parameters and the hierarchy are fixed definable data. The reflection theorem for definable hierarchies says that for every finite collection of formulas there is a closed unbounded class of ordinals such that
This is a schema of ZFC for each finite collection and class definition, not a purported truth predicate for all formulas over the universe at once.
Close under subformulas. For each existential subformula and each tuple in , if a witness exists in , take the least stage index containing a witness. There are only set-many parameter tuples and finitely many formulas. The Axiom schema of replacement therefore bounds all these least indices by an ordinal , chosen larger than . No definable selection of the witnesses themselves is needed.
Above any prescribed bound choose with , and put . Every tuple in lies in some , and each true existential instance for that tuple has a witness in . Induction over the subformulas now proves agreement between and : atomic formulas use the same membership relation, Boolean operations preserve agreement, and the existential step uses this witness property. Thus reflecting stages are unbounded.
For closedness, suppose reflecting stages have limit . Every tuple in lies in a reflecting stage below , and every true existential instance has a witness there. The same subformula induction proves reflection at . Hence the reflecting stages for the subformula-closed collection form a closed unbounded class, proving the Lévy reflection theorem in this relative form.
The printed inclusion-and-elementarity assertion is false if transitivity is required of the same submodel. Take the theorem of ZFC that combines the axiom of infinity and the Axiom of power set. Whenever satisfies this sentence, it contains , every subset of , and their actual power set . A submodel contains and , since these are uniquely definable in . If were transitive, it would contain every element of , contradicting countability by Cantor theorem.
The corrected conclusion uses an elementary embedding rather than elementary inclusion. By Lévy reflection theorem, choose with and with Extensionality true there. The Downward Lowenheim-Skolem theorem says that an infinite structure in a countable language has a countable elementary substructure. Apply it to obtain a countable . The membership relation on is externally well-founded, and elementarity makes it extensional. The Mostowski collapse theorem gives an isomorphism onto a countable transitive set. Hence
Indeed : rank induction gives for every . The crucial correction is that , rather than the inclusion of , is elementary. For a formula with free variables, apply this argument to its universal closure.

Articles by others on the same topic (0)

There are currently no matching articles.