Worked solution: Gödel and Cohen: the continuum hypothesis is independent of ZFC (1963)

A poset $\mathbb{P}$ satisfies the countable chain condition (ccc) if every antichain in $\mathbb{P}$ (a set of pairwise incompatible conditions, i.e. no two have a common extension) is countable. Cohen showed $\mathrm{Fn}(\aleph_2 \times \omega, 2)$ is ccc: by the Delta-system lemma, every uncountable family of finite domains contains two domains whose intersection is a common root; among the countably many assignments on that root, two conditions are therefore compatible. Hence every antichain is countable.

There is a general preservation theorem in forcing: if $\mathbb{P}$ is ccc, then forcing with $\mathbb{P}$ collapses no cardinals and adds no new countable sequences of ordinals that could witness a previously regular cardinal becoming singular or countable. Hence every cardinal of $V$, in particular $\aleph_1$ and $\aleph_2$, remains a cardinal — indeed remains $\aleph_1$ and $\aleph_2$ respectively — in $V[G]$.

With cardinals confirmed safe, the inequality $2^{\aleph_0} \ge \aleph_2 > \aleph_1$ established in the previous step is genuine and refers to the same $\aleph_1, \aleph_2$ throughout, so $V[G] \models \neg\mathrm{CH}$. Since $\mathbb{P} \in V$ and $V \models \mathrm{ZFC}$, this shows $\mathrm{Con}(\mathrm{ZFC}) \implies \mathrm{Con}(\mathrm{ZFC} + \neg\mathrm{CH})$: $\mathrm{CH}$ can never be proved from $\mathrm{ZFC}$ either.