= Solution
The predicate is defined by the <constructible hierarchy>:
$$
\boxed{L_0=\varnothing,\qquad L_{\alpha+1}=\operatorname{Def}(L_\alpha),\qquad
L_\delta=\bigcup_{\alpha<\delta}L_\alpha\quad(\delta\text{ limit}).}
$$
Here $\operatorname{Def}(A)$ consists of <subsets> of $A$ definable in the <set> structure $(A,\in)$ by a <first-order formula> with finitely many parameters from $A$. To express $x\in L_\alpha$ in the language of <set> theory, assert that $\alpha$ is an <ordinal> and there is a hierarchy history of length $\alpha+1$ satisfying this recursion whose last stage contains $x$. Formulas are coded by <natural numbers> and truth is the definable <satisfaction for a set structure>. <Transfinite recursion> gives a unique history. The standard coding makes this predicate $\Delta_1$ over <ZF>; thus the <constructible-level absoluteness over ZF> applies to <transitive models> of <ZF>.
Back to article page
