= Separation proof in the constructible universe
To separate a <subset> of a constructible <set> by a formula interpreted in the <constructible universe>, apply the <reflection theorem for definable hierarchies> to the formula and its subformulas. At a sufficiently large reflecting level containing the parameters, the desired <subset> is definable and belongs to the next <constructible hierarchy> level. The reflection proof uses least witness stages and ambient <Axiom schema of replacement>, so does not presuppose <Axiom schema of separation> within the <constructible universe>.
Back to article page
