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?

• 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$. Commented May 12, 2014 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? Commented May 11, 2014 at 16:01
• @sylvia This is the reflection theorem, and a basic application of Lowenheim-Skolem and the Mostowski collapse. Commented May 11, 2014 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.

• 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$. Commented May 11, 2014 at 17:40
• 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]$. Commented May 11, 2014 at 19:09