= Coded relative constructible stage
{title2=$S_X(\xi,B)$}
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>.
Back to article page
