Do we usually assume the consistency of ZFC when we use forcing? I used to think that to avoid philosophical problems in forcing one can assume consistency of ZFC. Then one obtains a set model $M$ contained in the von Neumann universe $V$. And then the generic filter as well as the extension $M[G]$ are also in $V$.
But apparently one cannot do this. Apparently $M$ will only ever be a model of a finite fragment of ZFC. Why? Why, if ZFC is consistent, does there not exist a set model $M$ of ZFC?
Thanks.
 A: $\mathsf{ZFC}$ cannot prove that it has models (thanks to Gödel), and even if you assume that $\mathsf{ZFC}$ has models, you still cannot assume that it has nice models (transitive "standard" models).  (Augment the language of set theory by adding constant symbols $c_0 , c_1 , \ldots$.  If $\mathsf{ZFC}$ is consistent, then by Compactness so is $T = \mathsf{ZFC} + ( c_{i+1} \in c_i : i \in \omega)$, and $T$ has no models in which the interpretation of $\in$ is well-founded.)
However, Levy Reflection says that given any finite list of axioms of $\mathsf{ZFC}$, there is a $\theta$ such that $V_\theta$ satisfies each of these axioms.  Then using Löwenheim-Skolem you can take a countable elementary submodel of a suitable $V_\theta$.  Collapsing this to a transitive set, you get a countable transitive model of the original list of axioms.
Of course, after this technically is recognised, you begin to think of your forcing as being done over $\mathbf{V}$, or perhaps $\mathbf{L}$ if you want $\mathsf{(G)CH}$ to hold in the ground model.
A: You are correct, and in fact one assumes more than just the consistency of $\sf ZFC$. In fact one assumes the consistency of a standard model of $\sf ZFC$ (which is a stronger assumption than just consistency).
One can do so, and many indeed do that.
But if we want that our proofs will go through in $\sf ZFC$ and not in $\sf ZFC+$"there is a standard model", then we cannot use models of the full theory at all. Luckily $\sf ZFC$ prove the existence of transitive models of any finite fragment of $\sf ZFC$, and we can take an arbitrary "large enough fragment" and work with that.
One can also use Boolean-valued [class] models and rid of all need reference to set models.
A: A standard way to get around this ‘difficulty’ is to work in the following conservative extension of $ \mathsf{ZFC} $:
$$
\mathsf{ZFC} \cup
\{ \text{$ \mathbf{M} $ is countable and transitive} \} \cup
\left\{ \phi^{\mathbf{M}} ~ \Big| ~ \phi \in \mathsf{ZFC} \right\},
$$
where $ \mathbf{M} $ is a constant symbol. This ‘innovation’ is due to Joseph Shoenfield and is discussed in detail in Kenneth Kunen’s book Set Theory: An Introduction to Independence Proofs. Of course, one can work with a syntactic forcing relation over the universe $ \mathbb{V} $ or with Boolean-valued models or ‘what not’, but I do not think that is where real posets come from. (Or do they?)
