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

For a transitive set $X$, use $L_0(X)=X$, $L_{\alpha +1}(X)=\mathrm{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.

If $\alpha$ is a nonzero limit ordinal and $Y\prec L_{\alpha }(X)$ with $X\cup \{X\}\subseteq Y$, the Mostowski collapse theorem sends $Y$ to $L_{\beta }(X)$ for some nonzero limit $\beta \le \alpha$ and fixes $X$ pointwise. The base is fixed by transitivity and inclusion of all its members. Transfer the relative constructible level recognition formula first by elementarity and then through the collapse isomorphism to identify its image. If $\rho =X\cap \mathrm{Ord}$, ordinal heights are $\rho +\alpha$ and $\rho +\beta$, giving the bound. Having only $X\in Y$ does not guarantee this base-fixing version.

For transitive sets $M,X$ with $X\in M$, a single first-order formula $\Phi (X)$ recognises the nonzero limit levels $L_{\alpha }(X)$. Require finite relation closure for set-theoretic coding, transitivity of $X$, that every element belongs to a coded relative constructible stage, and that every represented stage index has a larger represented index. Correct history codes have downward-closed indices with no maximum, hence form a nonzero limit ordinal $\alpha$. The exhaustion assertion and transitivity then give $M={\bigcup }_{\xi <\alpha }{L}_{\xi }(X)$. Conversely every limit level has the required closure, correct histories cofinal in its index, and exhaustion. This formulation does not assume ZF for an arbitrary input $M$ and does not replace finite coding closure with an unjustified internal constructibility assertion.

This first-order formula asserts the existence of a history function on $\xi +1$ starting at $X$, applying definable power set at successors and unions at nonzero limit ordinals, and ending at $B$. In a transitive set satisfying finite relation closure for set-theoretic coding, each history is correct by transfinite induction, so $B=L_{\xi }(X)$. Relation operations produce restrictions to shorter histories. Since stage histories appear below every limit constructible level, every history of length $\xi +1$ for $\xi <\alpha$ belongs to $L_{\alpha }(X)$ when $\alpha$ is a nonzero limit ordinal. This is the coding step behind relative constructible level recognition.

For a transitive set $X$, let $f_{\xi }$ be the history function $\eta \mapsto L_{\eta }(X)$ on $\xi +1$ in the relative constructible hierarchy. By transfinite induction, $f_{\xi }\in L_{\xi +k}(X)$ for some finite $k$, possibly depending on $\xi$. The base and successor steps follow by forming finite ordered pairs and adjoining the next entry, using $L_{\xi +1}(X)\in L_{\xi +2}(X)$. These operations require finitely many subsequent definable power sets.

At a nonzero limit ordinal $\lambda$, the inductive bounds put every earlier $f_{\eta }$ in $L_{\lambda }(X)$, since $\eta +k<\lambda$. This level satisfies finite relation closure for set-theoretic coding, independently of the availability of history functions. Consequently its coded relative constructible stage predicate computes the endpoints correctly. Finite pairing closure and the earlier histories show thatcontains exactly the pairs $⟨\eta ,L_{\eta }(X)⟩$ for $\eta <\lambda$. There are no extra indices: if $\eta \ge \lambda$ and $B=L_{\eta }(X)\in L_{\lambda }(X)$, increasing levels would give $B\in B$, contradicting Axiom of foundation. Thus $h=f_{\lambda }\upharpoonright \lambda$ is a definable subset of $L_{\lambda }(X)$ and belongs to $L_{\lambda +1}(X)$. Extracting its domain $\lambda$ and adjoining $⟨\lambda ,L_{\lambda }(X)⟩$ uses finitely many further operations, proving the induction step. Every nonzero limit $\alpha$ therefore contains all $f_{\xi }$ with $\xi <\alpha$, as required by relative constructible level recognition.