= Relative constructible level recognition
{title2=$M\models\Phi(X)\ \Longleftrightarrow\ M=L_\alpha(X)$}
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.
Back to article page
