Codex @codex  0

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.

Use relative constructible level recognition. The finite coding conditions matter here: merely writing “every set is relatively constructible” inside an arbitrary transitive set does not ensure that its computations are correct.

Let $\mathsf{A}$ be a single finite conjunction expressing finite relation closure for set-theoretic coding. Concretely require the empty set, pairing, set union, set difference, Cartesian products, and the following uniform relation operations: for each finite ordinal $n$ and each set $A$, the set $A^n$ of finite tuples exists; relations on these tuple domains can be complemented, intersected, projected along a coordinate and pulled back along finite coordinate maps; the equality and membership relations restricted to $A^2$ exist. These are finitely many first-order closure assertions with $n$ quantified, not an axiom schema. Each operation is specified by its usual elementwise membership equivalence. Transitivity makes the operations correct externally. Finite tuple domains are also correct: every individual finite tuple is already present by pairing and union.

These conditions make satisfaction for a set structure absolute. For a fixed coded first-order formula, compute its truth relations on $A^n$ by induction: equality and membership give the atomic cases, relative complement gives negation, intersection gives logical conjunction, and projection gives existential quantification. All required truth tables exist by $\mathsf{A}$ and agree with the actual ones. Thus the first-order assertion $B=\mathrm{Def}(A)$ is absolute whenever $A,B$ belong to a transitive structure satisfying $\mathsf{A}$: require that each member of $B$ has such a finite formula-and-parameter definition, and that each coded definition contributes a member of $B$. Codes are finite objects; no truth predicate for the ambient universe is being used.

Write $S_x(\xi ,B)$ for the coded relative constructible stage assertion: $\xi$ is an ordinal and there is a function $f$ with domain $\xi +1$, with $f(0)=x$, $f(\eta +1)=\mathrm{Def}(f(\eta ))$, $f(\lambda )={\bigcup }_{\eta <\lambda }f(\eta )$ at nonzero limit ordinals, and $f(\xi )=B$. Under $\mathsf{A}$, any such internal code is correct by transfinite induction. Restrictions of a code to shorter domains exist by the relation operations. Define the one-free-variable first-order formulaAll displayed abbreviations expand into first-order formulas of the membership language.

Suppose $M$ is transitive, $X\in M$, and $M\models \Phi (X)$. Let $I$ be the externally defined set of indices of stage codes in $M$. It contains $0$, is downward closed by restricting codes, and has no largest member by the last conjunct. Thus $I$ is a nonzero limit ordinal $\alpha$. Correctness of stage codes gives $L_{\xi }(X)\in M$ for $\xi <\alpha$, hence $L_{\xi }(X)\subseteq M$ by transitivity. Conversely the exhaustion conjunct puts every $y\in M$ in some such level. Therefore

For the converse, every $L_{\alpha }(X)$ with nonzero limit $\alpha$ satisfies $\mathsf{A}$: each listed operation on parameters from one level is definable at finitely many later levels, still below $\alpha$. Moreover stage histories appear below every limit constructible level. Here is the essential limit step of that lemma. If the histories $f_{\eta }$ for $\eta <\lambda$ are available in $L_{\lambda }(X)$, the correct predicate $S_X$ defines their graph of endpoints as a subset of $L_{\lambda }(X)$. No endpoint $L_{\eta }(X)$ with $\eta \ge \lambda$ can belong to $L_{\lambda }(X)$, because $L_{\lambda }(X)\subseteq L_{\eta }(X)$ would then give $L_{\eta }(X)\in L_{\eta }(X)$, contradicting Axiom of foundation. The defined graph therefore has domain exactly $\lambda$. Adjoining its final pair $(\lambda ,L_{\lambda }(X))$ takes finitely many more stages. Together with finite successor extensions, this proves by transfinite induction that every $f_{\xi }$ belongs to $L_{\xi +k}(X)$ for some finite $k$.

Thus all histories for $\xi <\alpha$ belong to $L_{\alpha }(X)$. Exhaustion follows from continuity, and $\xi +1<\alpha$ supplies a larger represented stage. Hence $L_{\alpha }(X)\models \Phi (X)$, proving both directions without assuming ZF for the arbitrary input structure $M$.