Relative constructible hierarchy (source code)

= Relative constructible hierarchy
{title2=$L_\alpha(X)$}

For a <transitive set> $X$, use $L_0(X)=X$, $L_{\alpha+1}(X)=\operatorname{Def}(L_\alpha(X))$ and unions at nonzero <limit ordinals>. The successor operation is the <definable power set>. Each level is transitive and the levels increase; moreover $X\in L_1(X)$. Their union is $L(X)$, an <inner model> of <ZF>. The initial-set convention differs from a hierarchy using a predicate, or one starting at $X\cup\{X\}$. <Axiom of choice> need not hold for an arbitrary base without an internally available <well-order>.