Gödel’s constructible universe, denoted by \(L\), is defined by transfinite recursion on the ordinals, similarly as \(V\), but at successor steps, instead of taking the power set of \(V_\alpha\) to obtain \(V_{\alpha +1}\), one only takes those subsets of \(L_\alpha\) that are definable in \(L_\alpha\), using elements of \(L_\alpha\) as parameters. Thus, letting \(\mathcal{P}^{Def}(X)\) to denote the set of all the subsets of \(X\) that are definable in the structure \((X,\in )\) by a formula of the language of set theory, using elements of \(X\) as parameters of the definition, we let