= Solution
An <inner model> of <ZF> is a <transitive class> $M$ containing every <ordinal>, with inherited membership, such that each <ZF> axiom holds with all quantifiers restricted to $M$. Here transitivity means $x\in y\in M\Rightarrow x\in M$. For a proper class this is an axiom-by-axiom assertion, not an internal truth predicate for the whole class. An <inner model> can have fewer <subsets> of a given <set> than the surrounding universe; it need not have the same <cardinals> or the same continuum function.
<Inner models> prove <relative consistency>. If a theory $T$ proves that a definable class $M$ satisfies every axiom of $S$, an inconsistency proof from $S$ could be relativized to $M$ and become an inconsistency proof from $T$. Thus \b[$\operatorname{Con}(T)\Rightarrow\operatorname{Con}(S)$]. This reasoning concerns formal interpretations and needs no assumption that a given model of $T$ is externally well-founded.
The central example is the <constructible universe>. Define
$$
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,
$$
where $\operatorname{Def}(X)$ contains exactly the <subsets> definable over $(X,\in)$ using parameters from $X$. <Satisfaction for a set structure> is definable, so this recursion is available in <ZF>. <Induction> shows that the levels are transitive and increasing: if $a\in L_\alpha$, the <subset> $\{x\in L_\alpha:x\in a\}$ is $a$, so $a\in L_{\alpha+1}$. The <ordinal> part of $L_\alpha$ is $\alpha$, giving all <ordinals> in $L$.
For completeness, the main axiom mechanisms explain why this example works. Finite <set> operations on constructible parameters are definable at finitely many further stages. For a fixed finite family of formulas and parameters, close a <sequence> of levels under their least constructible witness stages and take its <union>; <induction> on formulas gives a reflecting level. <Separation> of a constructible <set> then occurs at the next definability stage. For <replacement>, ambient <replacement> bounds the construction stages of the unique constructible outputs; a reflecting level above that bound makes the range definable. For the internal <power set> of $a\in L$, use ambient <separation> to form $\mathcal P(a)\cap L$, bound the construction stages of its members, and at a sufficiently high level define the family of all <subsets> of $a$ in that level. Thus the internal <power set> is constructible even though some ambient <subsets> may not be. <Foundation> is inherited by transitivity, and <infinity> comes from $L_\omega$ and its successor stages.
There is a canonical <well-order> of $L$: order by first construction stage, then by the least definition code and finite parameter tuple, using the previously constructed <well-orders> for parameters. Each <set> in $L$ can be well-ordered by the restriction of this set-like class order; hence $L$ satisfies <AC>. Moreover the hierarchy computed inside $L$ is the same hierarchy, because definability over a fixed <set> structure and limit unions are absolute. Thus $L$ satisfies $V=L$. The further <cardinal> analysis of this hierarchy, encapsulated in the <constructible universe theorem>, gives <GCH>. Consequently
$$
\boxed{\operatorname{Con}(\mathrm{ZF})\Longrightarrow\operatorname{Con}(\mathrm{ZFC}+V=L+\mathrm{GCH}).}
$$
This proves the <relative consistency> of choice, <CH> and <GCH>; in particular none can be refuted by <ZF> if <ZF> is consistent. The assertions here are internal to $L$: they do not assert <CH> in the ambient universe.
<Inner models> also isolate definable information. The <relative constructible universe> built with a <set> parameter retains that parameter and all <ordinals> while discarding unrelated <sets>. Such constructions help compare <relative consistency> strengths and identify which hypotheses survive passage to smaller universes; preservation of a large-cardinal property must be checked separately, not inferred merely from transitivity.
There is an important limitation, the <constructible-universe obstruction to a uniform inner-model proof of failure of choice>. Every <inner model> $M$ of <ZF> contains the ambient $L$. Indeed $L_\alpha^M=L_\alpha$ by <induction>: the same <set> structure has the same definable <subsets> at a successor stage, and both hierarchies take the same <union> at a limit. If the ambient universe satisfies $V=L$, this forces $M=V$. Thus <inner models> cannot uniformly produce a model of $\neg\mathrm{AC}$ or $V\ne L$ from every <ZF> universe. To prove the opposite independence directions one needs an outer-model or other interpretation technique, such as <forcing> or the non-well-founded symmetry construction in Question 2.
Back to article page
