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?


3 Answers 3


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.)

  • $\begingroup$ Thank you for the answer! I suppose I wasn't very clear in my question, but I was really looking for a more narrow answer - why don't the arguments for forcing over a countable transitive model (so no need for syntactic or Boolean-valued notions) hold when the model is just countable but not necessarily transitive? $\endgroup$
    – dorebell
    Jul 13, 2016 at 20:19
  • $\begingroup$ I have added an update addressing this. $\endgroup$ Jul 14, 2016 at 5:27
  • 3
    $\begingroup$ Thanks for the update! This seems to be getting to the heart of the matter. One more question - it seems that the definition of names, being internal to $M$, should work because $M$ "thinks" it's well-founded, but in defining the values, we need to either work with "real" set-membership (which is well-founded) and end up with something not having anything to do with the inductive construction in $M$, or attempt to induct on $M$-membership, but this time in the "real" world, where this isn't well-founded anymore. Is this correct? $\endgroup$
    – dorebell
    Jul 14, 2016 at 14:30
  • 5
    $\begingroup$ Yes, that is totally right. We want to induct on names, which is fine if we stay inside $M$, but since $G$ is involved, we are not staying inside $M$, and so there seems at first to be no way to carry out the recursion. Once having defined $M[G]$ by the Boolean-valued quotient process, however, then in fact we are able to carry out the recursion inside $M[G]$. But at that point, it isn't necessary, since we already have $M[G]$ by the other means. $\endgroup$ Jul 14, 2016 at 21:47
  • 1
    $\begingroup$ The Łoś theorem for Boolean ultrapower is the statement that $V^{\mathbb{B}}/U\models\varphi\iff[\![\varphi]\!]\in U$, and this does not use genericity. The existential case uses the fullness property of names, namely that $[\![\exists x\,\varphi(x)]\!]=[\![\varphi(\tau)]\!]$ for some name $\tau$. The supremum is realized. In particular, fullness shows that your situation does not happen. $\endgroup$ Feb 2, 2023 at 22:32

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].''

  • 1
    $\begingroup$ This looks great! So that there is an explanation on this site, would you be able to explain a main idea or two of this paper here? $\endgroup$
    – dorebell
    Jul 13, 2016 at 20:23

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.

  • 4
    $\begingroup$ Welcome to MathOverflow, Bill! $\endgroup$
    – Asaf Karagila
    May 4, 2017 at 19:06
  • $\begingroup$ This is the approach I used in Forcing for Mathematicians. $\endgroup$
    – Nik Weaver
    May 4, 2017 at 19:10
  • $\begingroup$ Yes, welcome to MO! Let me add that indeed, with this approach, there is in fact no need for $G$ to be generic, but only an ultrafilter on the Boolean algebra (which is a weak form on genericity on the poset), since that equivalence relation is exactly the same as the equivalence relation I mentioned. If $G$ is not generic, you still get a model $M[G]$ this way, and it satisfies the desired theory, and you get an elementary embedding from $M$ to the ground model of $M[G]$. But this map is surjective to the ground model of $M[G]$ if and only if $G$ is in fact $M$-generic. $\endgroup$ May 4, 2017 at 21:36
  • $\begingroup$ In particular, one can do this construction even when $G\in M$, and you still get a model $M[G]$ of the right theory. You only have to be careful about mapping $M$ into the new ground model, which consists of equivalence classes of names $\dot x$ for which some $p\in G$ forces $\dot x\in\check M$, and the new generic filter is the equivalence class of $\dot G$. $\endgroup$ May 4, 2017 at 21:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.