About proving that the Continuum Hypothesis is independent of ZFC

Question

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.

Answer 1

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

1. 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$.

2. 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.

Answer 2

As Asaf points out, we can still get the relative consistency results we want without "leaving" ZFC. But I think it is worth noting that there are natural extensions of ZFC in which the existence of ctm's of ZFC are provable, and thus in which we can carry out forcing arguments as is.

One natural extension arises from adding to ZFC a satisfaction predicate $Sat(x, y)$ with the usual Tarkian clauses for the connectives and quantifiers. For instance, we would add:

(&) $Sat(\phi\wedge\psi, a) \leftrightarrow Sat(\phi, a) \wedge Sat(\psi, a)$

where $a$ is an assignment function.

Once we have $Sat(x, y)$ in our language, it is natural to extend the replacement schema to formulas involving it. In the resulting theory we can prove that there are closed and unbounded $\alpha$ such that $V_\alpha$ is an elementary substructure of $V$. Each such $V_\alpha$ models ZFC, and it is then straightforward to get our ctm's using a Skolem hull argument on any one of them followed by the Mostowski collapse lemma.