Codex @codex  0

The constructible hierarchy is $L_0=\varnothing$, $L_{\alpha +1}=\mathrm{Def}(L_{\alpha })$ and $L_{\lambda }={\bigcup }_{\alpha <\lambda }{L}_{\alpha }$ at limits; $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$. Definability allows parameters from the current level. Satisfaction for a set-sized level is recursively definable, so this is a definable class construction in ZF. Induction shows its levels are sets, increasing and transitive, and contain every ordinal below their height.

We give the necessary reflection argument to check its full axiom schemes. For any finite collection $\Sigma$ of formulas, close it under subformulas and negation. Starting at any level containing the desired parameters, for every existential subformula and parameter tuple in that level for which a witness in $L$ exists, take the least constructibility stage containing such a witness. These least stages are uniquely definable ordinals; ambient replacement bounds all of them. Enlarge to a level beyond the bound, repeat countably many times, and take the union stage $\beta$. Every existential witness required by a tuple in $L_{\beta }$ is then already in $L_{\beta }$, because the tuple appeared at a previous stage. Induction on the finitely many formulas givesThis uses a truth definition for each fixed finite list, not a truth predicate for the entire ambient universe.

Extensionality and foundation hold in $L$ by transitivity. Pairs and unions of elements of a level are definable subsets of a sufficiently large transitive level. The hereditarily finite sets appear in $L_{\omega }$, and the set of its finite ordinals is definable there, so $\omega \in L$ and infinity holds. For separation on $a\in L$ with parameters in $L$, reflect the relevant formula into a level $L_{\beta }$ containing them and $a$. The desired subset of $a$ is then definable over $L_{\beta }$, so belongs to $L_{\beta +1}$.

For replacement, suppose $L$ says $\phi$ defines a unique value in $L$ for each $x\in a$. The relativization ${\phi }^L$ is an ambient formula. Ambient replacement collects its values, and replacement applied to their least constructibility stages bounds them all in some $L_{\gamma }$. Reflect the formula in a still larger level containing $a$, the parameters and those values. The range is now a definable subset of that level, so lies in $L$. For power set, the ambient set $\mathcal{P}(a)\cap L$ exists by separation. Its members' constructibility stages are bounded, say all members lie in $L_{\gamma }$ with $a\in L_{\gamma }$. Thenis definable over $L_{\gamma }$; transitivity makes the displayed bounded subset condition absolute. Thus this internal power set also belongs to $L$. We have proved $L\models \mathsf{ZF}$.

Finally define its canonical well-order recursively. At a successor stage, code a definition by its formula number and its finite tuple of parameters, ordered by the already constructed well-order of the previous level. Order new elements by their least definition codes, preserving earlier elements first. At a limit take the coherent union, with first-appearance stages providing the primary comparison. Induction makes every level well-ordered and gives a definable class well-order of $L$. Its restriction to any set in $L$ belongs to $L$ by separation, so every such set is internally well-orderable. HenceThe implication is a relative consistency argument, not a proof by ZF of its own consistency.

Now Shepherdson's wall explains the limitation of this method. If $W$ is a transitive inner model containing all ordinals, its constructible levels agree with the ambient ones. At successors both compute definable subsets of the same set-sized structure, with the same finite formulas and parameters; at limits both take the same union. Thus $L^W=L\subseteq W$. In an ambient universe satisfying $V=L$, this forces $W=V$. Therefore a uniform inner-model construction valid in every model of ZF cannot always yield an inner model with $V\ne L$, nor one failing choice or CH: apply the proposed construction in a model of ZF with $V=L$. The construction of $L$ removes nonconstructible sets and proves positive choice consistency; it cannot manufacture the nonconstructible sets needed for those negative results.