Why can we assume a ctm of ZFC exists in forcing Following Kunen's book, it makes clear that countable transitive models (ctm) exist only for a finite list of axioms of ZFC. So, why can we assume a ctm of the whole ZFC axioms exists and use it as our ground model? At the beginning of chapter VII, Kunen says that the formal proof is done by contraposition (assume ZFC+\neg CH is not consistent and show that ZFC is not consistent) but we can just "assume naively that we have a countable transitive M satisfying all of ZFC". I don't understand this point.
 A: This is to slightly elaborate on point 2 of Noah Schweiber's answer, since in my opinion this approach is often presented in a somewhat confusing manner which ommits some key subtelties.
Forcing constructions, as usually presented indeed seem to imply only a result of the form: "If there exists a countable transitive model of ZFC, then there exists a countable transitive model of T."
However, the usual forcing arguments can be adapted to yield the result: "If ZFC is consistent, then T is consistent." There are several ways to do it, some of them were mentioned in other answers or comments, but let me focus on the "consistency of finite subtheories" approach.
We want to show consistency of $ZFC + \phi$ using forcing. The usual arguments show that for any theory $T \subset ZFC$ which contains some basic set theory and has a transitive model, $T + \phi$ has a transitive model.
Notice that we can present $ZFC$ as a union of finite theories $ZFC_n$. Let's say that each of the theories contains only formulae of complexity $\Sigma_{n+17}$ (since we want all fragments considered to be large enough to make sense).
The "natural" argument works uniformly in $T$, so actually $ZFC$ (or some modest fragments of arithmetic) proves that for any $n$ if $ZFC_n$ has a transitive model, then $ZFC_n + \phi$ has a model.
Moreover, and this is the key point, the reflection principle also works uniformly in $ZFC$, so $ZFC$ formally proves the following:
$$\forall M \Big[(M \models ZFC) \rightarrow \forall n (M \models \exists M'  \ M' \text{ is a transitive model of $\Sigma_n$-true sentences }) \Big].$$
(Notice where the quantification over $n$ is placed.)
Combining the two observations, we obtain:
$$ZFC \vdash \forall M \Big[ (M \models ZFC) \rightarrow \forall n (M \models \exists M' \ M' \text{ is a model of $\Sigma_n$-true sentences $+ \phi$}) \Big]$$.
Notice that $M'$ - a model of $ZFC_n$ within $M$, is in fact a model of $ZFC_n$ itself. So in particular, we get:
$$ZFC \vdash \Big[(\exists M \ M \models ZFC) \rightarrow \forall n (\exists M' \ M' \models ZFC_n + \phi)\Big]$$
When presented with the proof of the reflection principle, people often ask why cannot we just apply compactness. As a matter of fact, now we can do precisely this, once we have used the intermediate model to quantify over the fragments for which we apply the reflection argument. This yields:
$$ZFC \vdash \Big[(\exists M \ M \models ZFC) \rightarrow (\exists M' \ M' \models ZFC + \phi)\Big].$$
The last one is formally a statement that consistency of $ZFC$ implies consistency of some other theories, proved as a formal statement in our metatheory by meta-massaging the natural proof as usually given in textbook.
A: Expositionally, forcing is (usually) easier to understand with a c.t.m. This does indeed lead to somewhat different results, such as

$(*)\quad$ If there is a countable transitive model of $\mathsf{ZFC}$ then there is a countable transitive model of $\mathsf{ZFC+\neg CH}$

as opposed to the snappier and more intuitive

$(**)\quad$ If there is a model of $\mathsf{ZFC}$ then there is a model of $\mathsf{ZFC+\neg CH}$

(which is of course equivalent to "$\mathsf{Con(ZFC)}\rightarrow\mathsf{Con(ZFC+\neg CH)}$" by the completeness theorem).
More precisely, thinking about c.t.m.s we see that $\mathsf{ZFC}$ proves $(*)$ but we do not immediately see that $\mathsf{ZFC}$ proves $(**)$.

There are, however, various ameliorating points here:

*

*First of all, $(*)$ is itself nontrivial; note that while the hypothesesized model is "special," so is the constructed model. So it's not really fair to say that it's weaker than $(**)$.


*More substantively, we could "stratify" forcing by finite subtheories of $\mathsf{ZFC}$. It turns out that we can write $\mathsf{ZFC}$ as a union of an increasing chain of finitely axiomatizable theories $\mathsf{ZFC}=\bigcup_{i\in\mathbb{N}}T_i$ with the property that each $T_i$ "supports forcing" in the appropriate sense: if $\mathcal{M}$ is a c.t.m. of $T_i$ then each generic extension of $\mathcal{M}$ is again a model of $T_i$. (And in fact this is overkill: it would be enough for our purposes to have each generic extension of a c.t.m. of $T_{i+1}$ satisfy $T_i$.) The reflection principle gives us c.t.m.s of each $T_i$, forcing thenn gives (for example) c.t.m.s of each $T_i+\neg\mathsf{CH}$, and finally the finiteness of proofs lets us conclude $\mathsf{ZFC}\not\vdash\mathsf{CH}$. This is the approach Kunen outlines if memory serves, and we can think of it as also subsuming Nik Weaver's suggestion in the comments of introducing a named c.t.m. of $\mathsf{ZFC}$ "inside (a conservative extension of) the theory."


*We could also simply develop forcing over arbitrary countable models of $\mathsf{ZFC}$. Remember that $\mathsf{ZFC}$ (and indeed much less) proves "If $\mathsf{ZFC}$ is consistent then it has a countable model," so hypothesizing countable models - unlike countable transitive models - doesn't actually take us beyond the (obviously necessary) hypothesis of $\mathsf{Con(ZFC)}$. This may seem difficult due to the use of recursion in defining the structure $M[G]$ (let alone $\Vdash$) and the reference to $V$ in verifying Regularity in $M[G]$, but since the whole point is that the forcing relation is definable inside the "base structure" these issues are easily surmountable. In fact, via Boolean-valued models we can develop forcing over arbitrary models full stop. In my opinion, this is the "right" approach to take since it really gets at the model-theoretic heart of the matter.
Whichever approach one takes, the point is that the c.t.m.-related issues are not actually that substantive, and blithely assuming the existence of a c.t.m. - while technically improper - makes it easier to see the actual mathematical intricacies of forcing (namely, how the combinatorial properties of the poset correspond to the logical properties of the extension that results from forcing with that poset).
A: I suggest you review the beginning of Chapter VII. In page 185, Kunen wrote:
"The formal structure of our proof of Con(ZFC)$\rightarrow$ Con(ZFC+V$\neq$ L) will be as follows......"
I think that answers your question.
