Fix and a formula . The reflection theorem for definable hierarchies supplies a stage containing these parameters at which the finitely many subformulas of have the same truth values as in , for arguments in .
This reflection can be proved in the ambient ZF without presupposing Axiom schema of separation in : starting at a stage containing the parameters, collect for each relevant existential subformula and every tuple in the current stage the least constructible stage in which a witness occurs, whenever a witness exists in . Ambient Axiom schema of replacement bounds these ordinals. Iterate these witness-stage bounds for steps and take their supremum. Induction on subformulas gives the required finite reflection at the resulting union stage. Only the least stage is chosen, so no ambient axiom of choice is needed.
Since is transitive and contains , the desired separated subset is
It is definable over with parameters there, so . Reflection gives . Hence ZF proves every Axiom schema of separation instance relativized to . This is a direct Separation proof in the constructible universe, not an appeal to the assertion being proved.
Use the transitive-model convention for “standard” in this assertion: the domain is a transitive set and membership is actual membership. A standard membership model of set theory without transitivity is a weaker notion and would not justify the asserted absoluteness. Ordinalhood is bounded-formula absolute, so the internal ordinals are precisely . Satisfaction for a set structure is absolute between transitive ZF models containing that structure: the domain, finite parameter tuples, formula codes and the recursive truth clauses are the same. Equivalently one may use the absoluteness of the predicate defining .
Transfinite induction now gives for each ordinal . At successors both computations use the same definable subsets of the same set structure; at limits they take the same union over all smaller ordinals, which belong to by transitivity. Thus
For a set-sized model of ordinal height , this is . The restriction to actual ordinals makes the printed union precise. Mere well-foundedness of a nontransitive membership substructure would not justify these absoluteness steps; transitivity is the intended standard-model convention.
Let be any transitive class model of ZF containing every ordinal. By part (b), all its internally computed constructible levels are the actual levels, and each belongs to, and is contained in, . Their union therefore gives . Using the permitted fact that , and that itself contains every ordinal, we conclude
The word class matters: a set cannot contain every ordinal. Set-sized standard models instead contain their own truncated constructible universe as described in part (b).

Articles by others on the same topic (0)

There are currently no matching articles.