= Solution
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 hierarchy>
$$
L_0=\varnothing,\qquad L_{\alpha+1}=\operatorname{Def}(L_\alpha),\qquad
L_\lambda=\bigcup_{\alpha<\lambda}L_\alpha,
\qquad L=\bigcup_{\alpha\in\operatorname{Ord}}L_\alpha.
$$
Here <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 $\operatorname{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 application
$$
\boxed{\operatorname{Con}(\mathsf{ZF})\Rightarrow\operatorname{Con}(\mathsf{ZFC}).}
$$
One 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. Consequently
$$
\boxed{L\models\mathsf{ZFC}+\mathsf{GCH},\qquad
\operatorname{Con}(\mathsf{ZF})\Rightarrow
\operatorname{Con}(\mathsf{ZFC}+\mathsf{GCH}).}
$$
All 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: \b[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.
Back to article page
