[proofplan]
Start with a countable transitive model $M$ of ZFC and form its internally constructible universe $L^M$. The relativized constructibility theorem says that $L^M$ is an inner model of $M$ satisfying ZFC and GCH, hence CH. Since $L^M$ is externally a subset of the externally [countable set](/page/Countable%20Set) $M$, and since constructibility is transitive through elements, $L^M$ is externally countable and transitive. Thus $L^M$ itself is the required countable transitive model of ZFC + CH.
[/proofplan]
[step:Construct the internally constructible universe of $M$]
Let $M$ be a countable transitive set such that $(M,\in)$ satisfies ZFC. Let $L$ denote Gödel's constructible universe, interpreted internally by the structure $(M,\in)$. Define $L^M$ to be the class, computed inside $M$, of all sets constructible over the ordinals of $M$; externally, we regard it as the set
\begin{align*}
L^M=\{x\in M : M \models x\in L\}.
\end{align*}
This display contains no TeX row separator; it is a single displayed formula. Because $L^M\subset M$ and $M$ is externally a set, $L^M$ is externally a set. Since $M$ is countable externally, every subset of $M$ is countable externally, so $L^M$ is countable externally.
[/step]
[step:Use Gödel constructibility to obtain ZFC and CH inside $L^M$]
Let GCH denote the generalized continuum hypothesis: for every infinite cardinal $\kappa$, there is no cardinal strictly between $\kappa$ and $2^\kappa$. By Gödel's constructibility theorem, relativized to the model $M$, the internally constructible universe $L^M$ is an inner model of $(M,\in)$ satisfying ZFC and GCH (citing a result not yet in the wiki: Gödel's theorem that $L$ satisfies ZFC + GCH). Here inner model means that, internally to $M$, the class $L^M$ is transitive, is contained in $M$, has the same ordinals as $M$, and satisfies the stated first-order axioms. Therefore
\begin{align*}
(L^M,\in)\models \mathrm{ZFC}+\mathrm{GCH}.
\end{align*}
This display contains no TeX row separator; it is a single displayed formula. Since GCH implies CH, it follows that
\begin{align*}
(L^M,\in)\models \mathrm{ZFC}+\mathrm{CH}.
\end{align*}
This display contains no TeX row separator; it is a single displayed formula.
[guided]
The purpose of passing from $M$ to $L^M$ is that constructibility gives a canonical inner model in which the continuum function is completely controlled. The theorem we use is Gödel's constructibility theorem in its relative form: whenever $M$ is a model of ZFC, the structure formed from the sets constructible inside $M$ is an inner model of $M$ and satisfies ZFC together with GCH.
Here $M$ satisfies ZFC by hypothesis, so the theorem applies to $M$. Its conclusion gives that $L^M$ is contained in $M$, is transitive internally to $M$, has the same ordinals as $M$, and satisfies
\begin{align*}
(L^M,\in)\models \mathrm{ZFC}+\mathrm{GCH}.
\end{align*}
This display contains no TeX row separator; it is a single displayed formula. The continuum hypothesis is the first instance of the generalized continuum hypothesis, namely the assertion that there is no cardinal strictly between $\aleph_0$ and $2^{\aleph_0}$. Thus any model satisfying GCH also satisfies CH. Therefore
\begin{align*}
(L^M,\in)\models \mathrm{ZFC}+\mathrm{CH}.
\end{align*}
This display contains no TeX row separator; it is a single displayed formula.
This is the only point where the deep set-theoretic input enters the proof; the remaining work is to check that $L^M$ has the external size and transitivity properties required by the theorem statement.
[/guided]
[/step]
[step:Verify that $L^M$ is transitive externally]
We show that $L^M$ is transitive as an external set. Let $y\in L^M$ and let $x\in y$. Since $L^M\subset M$, we have $y\in M$. Since $M$ is transitive externally and $x\in y$, we also have $x\in M$. Membership is absolute for the transitive structure $(M,\in)$ on elements of $M$, so $(M,\in)$ satisfies $x\in y$. Since $L^M$ is an inner model of $M$, it is transitive inside $M$; applying that internal transitivity to $y\in L^M$ and $x\in y$, the structure $(M,\in)$ satisfies $x\in L^M$. By the external definition of $L^M$, this means $x\in L^M$ externally.
This proves that every element of an element of $L^M$ again belongs to $L^M$, hence $L^M$ is transitive.
[/step]
[step:Take $L^M$ as the required model]
Let $N:=L^M$. The preceding steps show that $N$ is externally countable, externally transitive, and satisfies
\begin{align*}
(N,\in)\models \mathrm{ZFC}+\mathrm{CH}.
\end{align*}
This display contains no TeX row separator; it is a single displayed formula. Therefore there exists a countable transitive model of ZFC + CH. This proves the relative consistency statement.
[/step]
