Why do we need a transitive model in forcing arguments?

Question

One major approach to the theory of forcing is to assume that ZFC has a countable transitive model $M \in V$ (where $V$ is the "real" universe). In this approach, one takes a poset $\mathbb{P} \in M$, uses the fact that $M$ is countable to prove that there exists a generic set $G \in V$, then defines $M[G]$ as an actual set inside $V$ and proves it is a model of ZFC.

The downside to this approach is that a countable transitive model may not exist. For example, it is possible that $V = L$ and $V$ is a minimal model of ZFC, so that any smaller model $M \in V$ is non-standard. However, if we only want a countable model of ZFC, there is no problem. First, Gödel's completeness theorem shows that (assuming ZFC is consistent, of course!) there is some model $M_0 \in V$ of ZFC. Then, the Löwenheim-Skolem theorem guarantees that there is a elementary substructure $M \subseteq M_0$ which is countable in $V$. So $M$ is a countable model of ZFC, and therefore, there is a generic filter $G \in V$.

Can we continue the proof of forcing along these lines? Of course, transitivity is convenient for many reasons (such as showing that various formulas are absolute), but is it possible to go without it? Perhaps we would need to modify the construction of the $\mathbb{P}$-names and $M[G]$ by only considering elements that are actually in $M$.

EDIT To be a bit more clear, I believe that forcing can be done without a countable model at all, using either the syntactic approach or an approach via Boolean-valued models. My question is more humble. The arguments of forcing are very intuitive when $M$ is a countable transitive model; why don't the same (up to relativizing formulas to $M$) arguments work when $M$ is just countable?

Answer 1

Yes, one can undertake forcing without the transitivity assumption, and even the countability of the model is not important.

One of the standard ways to do this is with the Boolean-valued model quotient construction, which has been described in many places. Basically, given a forcing notion $B$, a complete Boolean algebra (take the completion if you have only a partial order), form the class of all $B$-names, and then define the Boolean values $[\![\varphi]\!]^B$. This can be done internally to any model $M$. If $U\subset B$ is any ultrafilter — no need for genericity of any kind, and even $U$ inside $M$ is fine — then you define the quotient $M^B/U$ by the equivalence relation $$\sigma =_U\tau\quad\iff\quad[\![\sigma=\tau]\!]\in U,$$ which is a congruence with respect to the relation $$\sigma\in_U\tau\iff [\![\sigma\in\tau]\!]\in U.$$ One then verifies the Łoś theorem property that $M^B/U\models\varphi\iff[\![\varphi]\!]\in U$, and so $M^B/U$ is a model of any statement whose Boolean value is in $U$.

To construct a model of ZFC+$\neg$CH, for example, start with any model $M\models\text{ZFC}$, and let $U\subset B$ be any ultrafilter in the Boolean algebra arising from Cohen's forcing to add $\aleph_2$ many Cohen reals. The model $M^B/U$ will satisfy ZFC+$\neg$CH. No need for $M$ to be countable or transitive!

You can find further extensive details in my paper, Well-founded Boolean ultrapower as large cardinal embeddings, including a discussion of what I call the naturalist account of forcing, which describes how one can take the common set-theorist's talk of "forcing over $V$" at face value.

Update. Let me respond to your comment and clarified question. You want to know where the argument commonly used with countable transitive models goes wrong without those assumptions. So let me explain.

• Countability is clearly used in order to find the generic filter. Strictly speaking, one doesn't need that the entire model is countable, but rather only that the model $M$ has only countably many dense subsets of the forcing notion $P$ being used for the forcing. For example, one can easily find generic filters for any forcing notion in an $\omega_1$-like model, which is an uncountable model all of whose rank initial segments are countable. More generally, it suffices if there are only countably many maximal antichains for the forcing, since meeting these suffices for genericity. One can relax this a bit in certain cases. For example, if you have Martin's axiom or some other forcing axiom, and if $M$ has fewer than continuum many open dense sets for a forcing notion P that happens to be ccc in the ambiant universe, then it will be instance of the forcing axiom to know that there is an $M$-generic filter. And similarly with proper forcing and PFA and so on. So these are some ways in which you can dispense with the countability assumption and still get a generic filter.

• Transitivity. The use of transitivity in the CTM approach to forcing is used critically in the definition of what $M[G]$ is. Namely, one usually defines $M[G]$ to consists of all the interpretations of names $\tau$ in $M$ by $G$, defining the value $$\newcommand\val{\text{val}}\val(\tau,G)=\{\val(\sigma,G)\mid\exists p\in G\ \langle\sigma,p\rangle\in \tau\}.$$ This definition takes place by $\in$-induction in a realm where both $M$ and $G$ exist. One cannot seem to carry out this induction on names if the model is not $\in$-standard or at least well-founded, and so this is the main point of failure with the usual CTM approach to forcing. Without transitivity or at least well-foundedness, we don't seem to know exactly what $M[G]$ should mean. This problem is addressed in the Boolean-valued model quotient construction by defining $M[G]$ as a quotient by an equivalence relation, rather than by the $\in$-inductive value procedure. Furthermore, if $G$ is $M$-generic for a non-well-founded model $M$, then indeed after forming the model $M[G]$ by the quotient construction $M^B/G$, then inside $M[G]$ one can see that it arises internally via the values-of-names construction. But the point is that without having first provided an alternative definition of what $M[G]$ is, one doesn't seem at first able to carry out that name-value process, because the induction takes place in context with both $M$ and $G$ already available. (And this subtle point, I believe, seems to be the answer to your question as updated by the revision.)

Answer 2

This is really a comment on Hamkins answer, but I'm not permitted to make comments so I'll write it as an answer.

Using the standard Schoenfield machinery for forcing, there is no need for a well founded model. The theory of forcing is developed entirely inside the model $M$, including the definition of the class of names and the forcing relation. This uses the axiom of foundation inside $M$, but not external well foundedness. Given a externally defined generic set $G$, then, $M[G]$ is just the set of equivalence classes of names under the relation $\dot x \equiv \dot y \iff \exists p\in G ( M\vDash p\vdash \dot x = \dot y)$.

This is, of course, essentially equivalent to Hamkins' answer.

Answer 3

You may look at the paper ``Forcing with non-wellfounded models''. Australas. J. Log. 5 (2007), 20–57, by Paul Corazza:

Here is the abstract of the paper:

We develop the machinery for performing forcing over an arbitrary (possibly non-well-founded) model of set theory. For consistency results, this machinery is unnecessary since such results can always be legitimately obtained by assuming that the ground model is (countable) transitive. However, for establishing properties of a given (possibly non-well-founded) model, the fully developed machinery of forcing as a means to produce new related models can be useful. We develop forcing through iterated forcing, paralleling standard steps of presentation in [K. Kunen, Set theory, North-Holland, Amsterdam, 1980] and [T. J. Jech, in Handbook of Boolean algebras, Vol. 3, 1197–1211, North-Holland, Amsterdam, 1989].''