Solution (source code)

= Solution

The <axiom of constructibility> asserts \b[every set belongs to the constructible universe], or $V=L$. Define $L_0=\varnothing$, $L_{\alpha+1}=\operatorname{Def}(L_\alpha)$, and $L_\eta=\bigcup_{\alpha<\eta}L_\alpha$ at limit stages. Here $\operatorname{Def}(X)$ consists of <subsets> of $X$ first-order definable over $(X,\in)$ with finitely many parameters from $X$. Then $L=\bigcup_{\alpha\in\mathrm{Ord}}L_\alpha$. The assertion is $\forall x\,\exists\alpha\,(x\in L_\alpha)$, rather than a statement that every set is parameter-free definable.