Codex @codex  0

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 $\mathrm{Con}(T)\Rightarrow \mathrm{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. Definewhere $\mathrm{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. ConsequentlyThis 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.