The Constructible Hierarchy satisfies:

More precisely, we prove for arbitrary :

where is the set theoretic universe . The relation can be encoded in for any such that:

in the meta-theory (even when is a non-standard model). Thus we usually don’t concern ourselves with these issues.

Proof

We examine the Axioms of ZF individually.

Structural axioms

Any Transitive Model satisfies Axiom of Extensionality and Axiom of Foundation. Also is Absolute, and satisfies Axiom of Infinity, we also get Axiom of Infinity for all .

Functional Axioms

Pair and Union

The operations and are Absolute Operations for a Sufficiently Strong . So we only need to prove

Assuming , take some such that . Consider:

Form

The union is essentially the same.

Powerset

This is more complicated, because Powerset Axiom is not Absolute. (But if it was Absolute, it would be hopeless to find a powerset in a countable model) Note that is Absolute. Thus if then . Also clearly as is Transitive. Thus our candidate is . If then satisfies the conditions of the powerset axiom. Define

By Axiom of Replacement this is a set, and it is a set of ordinals, so it has to have an upper bound so there is some such that , so . Let

then and thus .

Separation

Axiom of Separation For any formula , we need the set

where are parameters. Take the formula

Then

This only works if and is Absolute between and . Apply Lévy Reflection Theorem to find such . Thus

and so separation holds.

Replacement

Axiom of Replacement Let be a formula such that

Then we need

Fix some and such that . Let be a formula obtained from by relativizing all quantification to . Then (for fixed ) if and only if Using replacement, find such that

Form the set of ordinals

and take its supremum . Then take by Lévy Reflection Theorem such that is absolute between and . Then

so . But then is the witness of replacement in !