About proving that the Continuum Hypothesis is independent of ZFC In Mathematical Logic, we were introduced to the concept of forcing using countable transitive models - ctm - of $\mathsf{ZFC}$. Using two different notions of forcing we were able to build (from the existence of a "basic" ctm) two different ctm's, where one of them verifies the continuum hypothesis ($\mathsf{CH}$), and the other verifies its negation.
My question is the following. Does this prove that $\mathsf{CH}$ is independent of $\mathsf{ZFC}$? It seems to me that the only thing this proves is: "If there is a ctm of $\mathsf{ZFC}$ then $\mathsf{CH}$ is independent of $\mathsf{ZFC}$". And, well, we cannot prove in $\mathsf{ZFC}$ that there is a ctm of $\mathsf{ZFC}$, since that would imply that $\mathsf{ZFC}$ proves its own consistency!
What am I missing here? Is it enough to assure the existence of a ctm in some "universe" different from $\mathsf{ZFC}$? Does this even make sense?
Thank you in advance.

Yes, you are right. However there are two ways around this.

*

*We can use Boolean-valued models. These are definable classes, and we can show that for a statement $\varphi$, if there is a complete Boolean algebra $B$ such that in the Boolean-valued model $V^B$, the truth value of $\varphi$ is not $1_B$ then $\varphi$ is not provable from $\sf ZFC$.
Then we can find such $B$ for which the continuum hypothesis doesn't attain the value $1_B$.


*We can argue that any finite fragment of $\sf ZFC$ has a countable transitive model. If $\sf CH$ was provable then it was provable from some finite fragment of $\sf ZFC$. Add to that fragment the axioms needed to develop the basics of forcing needed for the proof, and this theory is a finite subtheory which has a countable transitive model, over which we can force and show that the finite subtheory is preserved. However $\sf CH$ is false there. So every finite fragment of $\sf ZFC\cup\{\lnot CH\}$ is consistent, therefore $\sf ZFC\cup\{\lnot CH\}$ is consistent.
