Independence of the continuum hypothesis from ZFC

Let $\mathrm{ZFC}$ be first-order Zermelo–Fraenkel set theory with choice and $\mathrm{CH}$ the continuum hypothesis as a sentence of set theory. If $\mathrm{ZFC}$ is consistent, then $\mathrm{ZFC}$ neither proves nor refutes $\mathrm{CH}$:

This is the resolution of Hilbert's first problem: Gödel (1940) and Cohen (1963) together.

Formalization Note Consistency is satisfiability and $\vdash$ is semantic consequence $\models$ (truth in every model with universe in Type); by Gödel's completeness theorem these agree with the syntactic notions.