Henkin's Model Existence Theorem says that, if $T$ is a consistent theory, then there exists some set $S$ such that $S \models T$.
Suppose we are trying to prove the theorem $\text{Con}(ZFC) \rightarrow \text{Con}(ZFC + \neg CH)$. Are the following steps a correct way to start?
- Assume $\text{Con}(ZFC)$.
- Use Henkin's Model Existence Theorem to get a pair $(M,E)$ with $(M,E) \models ZFC$.
- Use the Downward Löwenheim-Skolem Theorem to get a pair $(M', E')$ with $|M'| = \aleph_0$ and $(M',E') \models ZFC$.
In Set Theory (2011), Kunen instead forces using models of a finite subtheory $\Omega \subset ZFC$ instead of models of $ZFC$ itself. Considering the steps I outlined above, why is it necessary to use a finite subtheory? Is the finite subtheory helpful for getting a model that is transitive as well as countable? Or do the steps above not work for some reason?
Best Answer
Yes, because the standard formalism for forcing that Kunen uses starts with a countable transitive model of $\sf ZFC$, rather than just any countable model, more care is needed. Whether there is a transitive model of $\sf ZFC$ is independent from $\sf ZFC + Con(ZFC),$ though once you have one, you can get a countable transitive model by Lowenheim-Skolem + Mostowski collapse.
On the other hand, the reflection schema allows you to construct, in $\sf ZFC$ alone, a countable transitive model of any finite subtheory of $\sf ZFC$. Analyzing the forcing formalism, if we have an arbitrary finite fragment $T$ of $\sf ZFC + \lnot CH,$ it's possible to find a finite fragment $T'$ of $\sf ZFC$ such that we can, working in $\sf ZFC,$ construct a countable transitive model $M$ of $T'$ and show the generic extension $M[G]$ satisfies $T.$
If $\sf ZFC + \lnot CH,$ were inconsistent, there would be some finite fragment witnessing this, and then the above procedure would produce a contradiction in $\sf ZFC$ alone. So, as a bonus, this is no mere infinitary proof of $\sf Con(ZFC)\to Con(ZFC+\lnot CH)$ using model theory within $\sf ZFC$, but rather a finitary syntactic proof of $\sf Con(ZFC)\to Con(ZFC+\lnot CH)$.
On a side note, it is possible to carry out an independence proof that starts out like you suggested. Note that in the transitive approach, the construction of $M[G]$ uses the (external) well-foundedness of $M$ in an essential way. An analogous construction in the not-necessarily-well-founded case is possible, but more complicated$^*$. Between that complication and the fact that transitive models are nicer to work with for all sorts of reasons, the transitive models approach is generally favored as an introduction, despite the mild metamathematical hiccups it causes.
$^*$ One approach that works is to construct the relevant Boolean-valued model inside $M$ and then take a quotient of it by any ultrafilter. But then again, Boolean-valued models already produce a nice relative consistency proof on their own. See also this answer for a brief description, and JDH's answer to the same question for more on the BVM approach.