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

-
One way of viewing independence results is that that they give you a computer program that will convert any proof of CH or not-CH into a proof of $0 = 1$. –  hot_queen May 12 at 16:38

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.

-
this is a very elegant reasoning. i am just curious (not skeptical, though!) about the we can argue that any finite fragment of ZFC has a countable transitive model... how would one argue that? perhaps you can provide some references? –  sylvia May 11 at 16:01
@sylvia This is the reflection theorem, and a basic application of Lowenheim-Skolem and the Mostowski collapse. –  Andres Caicedo May 11 at 16:13

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.

-
See also this closely related answer by Andreas Blass. –  Andres Caicedo May 11 at 16:46
Thanks, Andres. I'd forgotten that answer by Andreas. Just to be clear: this kind of move is basically folklore and has been around for quite a while. –  GME May 11 at 16:51
In the same spirit, perhaps it's worth mentioning Feferman's addition of a constant $U$ with the axioms that $U$ is a countable transitive set, and all the axioms of $\sf ZFC$ relativize to $U$. Surprisingly this is a conservative extension of $\sf ZFC$. –  Asaf Karagila May 11 at 17:40
It's not entirely clear to me that it's in the same spirit, since ctm's aren't provable in Feferman's theory. Is there another reason working in that theory (for the purpose of forcing) is somewhat easier than the strategies you outline in your answer? –  GME May 11 at 17:52
It's a meta-theorem that there is a countable transitive model of $\sf ZFC$. But $U$, by all standards is a countable transitive model, and every axiom of $\sf ZFC$ is true there. Then you can construct generic filters to posets from $U$, and prove - axiom by axiom - that the axioms of $\sf ZFC$ are true in $U[G]$. –  Asaf Karagila May 11 at 19:09