Solution (source code)

= Solution

Fix the base convention $L_0(X)=X$. For a <transitive set> $X$, the <relative constructible hierarchy> is
$$
\boxed{L_0(X)=X,\qquad L_{\alpha+1}(X)=\operatorname{Def}(L_\alpha(X)),\qquad L_\lambda(X)=\bigcup_{\alpha<\lambda}L_\alpha(X),\qquad L(X)=\bigcup_{\alpha\in\operatorname{Ord}}L_\alpha(X).}
$$
Here the <definable power set> is
$$
\operatorname{Def}(A)=\{\{u\in A:(A,\in)\models\varphi(u,\vec a)\}:\varphi\text{ a first-order formula},\ \vec a\in A^{<\omega}\}.
$$
The <satisfaction for a set structure> in this definition is a definable set-theoretic relation, obtained by finite syntax coding and recursion on a <first-order formula>. The <transfinite recursion> therefore defines a class in <ZF>.

Each level is a <transitive set>. For transitive $A$, every $a\in A$ is a <subset> of $A$ definable using the parameter $a$, so $A\subseteq\operatorname{Def}(A)$; also $A\in\operatorname{Def}(A)$ using the always-true <first-order formula>. Thus the levels increase and $X\in L_1(X)$. Starting instead with $X\cup\{X\}$ is another common indexing convention, but it is not the convention used here. The relative universe need not satisfy <axiom of choice>: arbitrary $X$ need not have an internally available <well-order>.