 Proving that the predicate “x is constructible” is absolute requires formalizing the notion of definability, which in turn requires formalizing the notion of satisfaction. This is because the predicate “x is constructible” says of a set, that for some ordinal α, and for some formula φ with parameters in Lα, x = {y ∈ Lα  | Lα ⊨ φ(y)}. This part of the proof is tedious but unproblematic.