Codex @codex  0

For a transitive model $M$ of ZFC and $\alpha \in M\cap \mathrm{Ord}$, the internally computed constructible hierarchy agrees with the ambient level: $L_{\alpha }^M=L_{\alpha }$. Satisfaction for a fixed set structure is computed from the same finite formulas and the same domain in both universes. Transfinite recursion then proves agreement at successors and limits. If $\theta =M\cap \mathrm{Ord}$, it follows that $L_{\theta }\subseteq M$.

Every set belongs to some level of the constructible hierarchy. The assertion is $\forall x\exists \alpha (x\in L_{\alpha })$, not that each set is definable without parameters. The constructible universe theorem supplies a relative-consistency model of this assertion from ZFC.

For $A\in L$, its constructible power set isUnlike the single-stage definable power set $\mathcal{D}(A)$, it includes subsets of $A$ appearing arbitrarily late in the constructible hierarchy.

The definable power set $\mathcal{D}(X)=\mathrm{Def}(X)$ consists of the subsets of $X$ definable over the first-order structure $(X,\in )$ by a first-order formula with parameters from $X$. Satisfaction for a set structure makes this a definable operation in ZF. Iterating it produces the constructible hierarchy and the relative constructible hierarchy; their unions are the constructible universe and the relative constructible universe.

Inside the constructible universe, every hereditarily countable set appears in a countable level of the constructible hierarchy. Take a countable elementary substructure of a sufficiently large $L_{\eta }$ containing its transitive closure pointwise. The condensation lemma for the constructible universe identifies the collapse with $L_{\beta }$ for countable $\beta$, and the collapse fixes the original set. Conversely, a countable-indexed level is countable inside the constructible universe.

An inner model of a universe of ZF is a transitive class $M$ containing every ordinal and satisfying the required set-theoretic axioms with the inherited membership relation. Transitivity means that every member of a member of $M$ belongs to $M$. Requiring all ordinals distinguishes an inner model from a transitive set first-order model such as $V_{\kappa }$: a set first-order model has bounded ordinal height. One may specify an inner model of ZF, ZFC or a stronger theory; choice is not built into the term unless specified.

The fundamental example is the constructible universe. Form the constructible hierarchyHere definable power set means subsets definable over the set structure $(L_{\alpha },\in )$ by first-order formulas with finitely many parameters from that level. Each level is transitive, the levels increase, and $\mathrm{Ord}\cap L_{\alpha }=\alpha$, by induction. Thus $L$ is transitive and contains all ordinals.

The construction supplies a definable well-order: order objects first by their earliest construction stage, then by a least first-order formula code and a finite tuple of parameters in the already constructed level's well-order. Recursively extend the earlier well-order at each successor stage and unite compatible orders at limits. First-order formula codes and finite tuples of well-ordered parameters are well-orderable. This yields a canonical global ordering definable within $L$; its restrictions to sets will give choice once the ZF axioms are checked.

For that check, a useful reflection argument is explicit. Given finitely many first-order formulas and a starting level, pass to a higher level containing witnesses for their existential subformulas on all parameter tuples from the current level, choosing least witnesses in the canonical order. There are set-many tuples, so ambient replacement bounds their witness stages. Repeat for $\omega$ steps and take the union level $L_{\theta }$. Every relevant witness with parameters in that level appears at a later step. Induction on first-order formulas, with this witness property for the existential case, proves that $L_{\theta }$ reflects the chosen finite list of first-order formulas of $L$.

Separation on a constructible set is then definability over a sufficiently large reflecting level, so its subset appears at the next level. For replacement, reflect the first-order formula specifying a functional image and its required existence statements. All inputs belong to a level containing the domain as a set; all their unique outputs then lie in one reflecting level. The image is definable there and hence is constructible. For power set, the ambient set of constructible subsets of $x$ has bounded construction stages by replacement in the ambient universe. At a level containing them all, this internal collection is definable by the bounded condition $y\subseteq x$, and therefore is itself in $L$. Pairing, union and axiom of infinity follow directly from definability over sufficiently large levels, while extensionality and foundation follow from transitivity. Thus $L\models \mathsf{ZF}$, and its canonical ordering gives $L\models \mathsf{AC}$.

This proves the important relative-consistency applicationOne does not conclude that choice is true in the original universe. Instead the inner model supplies a possibly smaller universe in which choice holds.

Constructibility also supplies GCH. Here is the cardinal-counting argument, making clear the role of the condensation lemma for the constructible universe. Work inside $L$. If $x\subseteq \kappa$ is constructible, take a large limit $L_{\theta }$ containing $x$ and an elementary hull of $\kappa \cup \{\kappa ,x\}$ of size $\kappa$. Its transitive collapse is $L_{\beta }$ by condensation. The collapse fixes every ordinal below $\kappa$, and hence fixes $x$ and $\kappa$. Since the hull has size $\kappa$, $\beta <{\kappa }^{+}$. Therefore every constructible subset of $\kappa$ appears below $L_{{\kappa }^{+}}$.

The condensation fact expresses the rigidity of this definability construction: first-order formula codes, finite parameter tuples and satisfaction in set-sized lower levels are preserved by the collapse. Inducting over the hull's ordinal indices identifies each collapsed lower level with the corresponding $L$-level; elementarity supplies every definable subset coded by parameters in that collapsed lower level. Taking unions identifies the entire collapsed hull with a level $L_{\beta }$.

Induction on construction stages gives $|L_{\gamma }|\le |\gamma |+{\aleph }_0$: each successor has only countably many first-order formula schemes with finite parameter tuples, and limits take unions. Hence $|L_{{\kappa }^{+}}|={\kappa }^{+}$ for infinite $\kappa$. The preceding containment gives $2^{\kappa }\le {\kappa }^{+}$ in $L$, and Cantor's theorem gives the reverse inequality. ConsequentlyAll these cardinal computations are internal to $L$; they need not equal the ambient cardinal computations.

Inner models are also useful for analyzing stronger axioms. If $\kappa$ is inaccessible in $V$, it remains an uncountable regular cardinal in $L$, because a shorter cofinal sequence in $L$ would already be one in $V$. For each ordinal $\lambda <\kappa$, its constructible subsets are fewer than $\kappa$ even in the internal cardinal comparison: in $V$, $\mathcal{P}(\lambda )$ has size below $\kappa$, so its constructible part cannot have an $L$-well-order of length at least $\kappa$. Thus it remains strong limit. Accordingly $L$ supplies relative-consistency information compatible with inaccessibles and GCH. Stronger embedding or measure properties require extra analysis, since the witnessing objects may disappear upon passing to an inner model.

There is a useful limitation: no uniform inner-model construction can refute choice from every starting ZF universe. Every inner model $M$ of ZF contains the ambient $L$. Indeed, induction gives $L_{\alpha }^M=L_{\alpha }$: the same set-sized level has the same satisfaction relation for definitions, and limit stages take the same unions. If the starting universe already satisfies $V=L$, any inner model containing all ordinals must therefore be the whole universe, where choice holds. To obtain a choice-failing first-order model uniformly one needs a different method, such as the symmetry restriction in the preceding solution. Inner-model arguments establish consistency and preservation through carefully controlled smaller universes; they do not freely manufacture arbitrary desired axiom failures.

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.

The predicate is defined by the constructible hierarchy:Here $\mathrm{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.

The Von Neumann hierarchy and the constructible hierarchy are defined by transfinite recursion:The union clauses apply to nonzero limit ordinals. The definable power set $\mathrm{Def}(L_{\alpha })$ consists of subsets definable over $(L_{\alpha },\in )$ by a first-order formula with finitely many parameters from $L_{\alpha }$. Definability over that structure is essential; it is not unrestricted definability in the ambient universe. The full constructible universe is $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$.

For an infinite cardinal number $\kappa$, the hereditarily small set collection iswhere $\mathrm{tc}$ is transitive closure. Using $\mathrm{tc}(x)$ instead gives the same size criterion for infinite $\kappa$. This bounds the whole membership ancestry, not just $|x|$.

The argument in part (a) established $L_{\alpha }\subseteq L_{\alpha +1}$ for every ordinal $\alpha$. A transfinite induction on $\beta$ now proves that every earlier level is contained in $L_{\beta }$. If $\beta =\gamma +1$, use the inductive inclusions into $L_{\gamma }$ followed by $L_{\gamma }\subseteq L_{\gamma +1}$. At a limit stage, every earlier level is one of the sets in the defining union. Equality of indices is trivial. ThusThe constructible hierarchy is a nondecreasing family of sets.

The constructible hierarchy is defined by transfinite recursion using the definable power set. With parameters permitted in the internal definitions, write $\mathrm{Def}(A,1)$ for the definable subsets of $A$. ThenIts class union is the constructible universe $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$. Only subsets definable over $(L_{\alpha },\in )$ using a first-order formula and finitely many parameters from $L_{\alpha }$ enter at a successor stage.

The definable power set $\mathcal{D}(A)$ performs one definability step over the single structure $(A,\in )$, whereas the constructible power set ${\mathcal{P}}^L(A)$ contains subsets of $A$ created at arbitrarily late stages of the constructible hierarchy.

For the concrete case $A=\omega$, there are only countably many first-order formulas and finite tuples of natural-number parameters, so $\mathcal{D}(\omega )$ is a countable set. In contrast, the constructible universe satisfies ZFC, and Cantor theorem makes its full power set ${\mathcal{P}}^L(\omega )$ uncountable inside $L$. Consequentlyso the two notions do not agree in general.

Fix $a\in L$. Inside the ambient transitive model $M$, the Axiom of power set makes the collection of constructible subsets of $a$ a set. For each such subset $x$, choose the least stage of the constructible hierarchy at which $x$ appears. The Axiom schema of replacement and the supremum of a set of ordinals give an ordinal $\beta$ bounding all these stages; enlarge $\beta$ so that $a\in L_{\beta }$.

Nowis definable over $L_{\beta }$ with parameter $a$. It therefore belongs to the definable power set $\mathcal{D}(L_{\beta })=L_{\beta +1}\subseteq L$. This set contains exactly the subsets of $a$ that belong to the constructible universe, so it witnesses the Axiom of power set in $L$. Therefore $L\models$ Power Set.

Work in the ambient universe and let $a,u\in L$. SupposeFor each $x\in a$, let $y_x$ be this unique witness. The relativization ${\phi }^L$ is a first-order formula, so the ambient Axiom schema of replacement collects the witnesses $y_x$ into a set. Every witness lies in the constructible hierarchy, hence there is an ordinal $\alpha$ such thatFor example, take the supremum of one constructible rank for each witness and then increase it by one.

The set $L_{\alpha }$ itself belongs to $L_{\alpha +1}\subseteq L$. Taking $b=L_{\alpha }$, every $x\in a$ has a witness $y\in b$ satisfying ${\phi }^L(x,y,u)$. Thereforewhich is the stated instance of Replacement.

The constructible hierarchy is defined by transfinite recursion:when $\lambda$ is a limit ordinal. Its union over all ordinals is the constructible universe $L$.

To separate a subset of a constructible set by a formula interpreted in the constructible universe, apply the reflection theorem for definable hierarchies to the formula and its subformulas. At a sufficiently large reflecting level containing the parameters, the desired subset is definable and belongs to the next constructible hierarchy level. The reflection proof uses least witness stages and ambient Axiom schema of replacement, so does not presuppose Axiom schema of separation within the constructible universe.