There are some interesting questions and answers on the site discussing the different approaches to forcing in set theory, and I understand that the two most important are the ones using countable transitive models (ctm) and Boolean valued ones (bvm), respectively.

My question is primarily about which of those two approaches appears in the literature more often, especially in research articles. I know that it might be difficult to answer, but perhaps an educated guess by the users of the site will be enough for me.

The context of this question is that my team is working on a formal verification of forcing using the ctm approach, and it is important for us to be able (to the extent possible) to represent the actual practice of the subject. It is to be noted that a full formalization of the bvm approach was recently completed by Han and van Doorn.

  • 5
    $\begingroup$ I know four approaches to forcing: using partial orders, using Boolean valued models, topological approach and categorical approach. For me working with partial orders is the most convenient , but sometimes, it is easier to use the Boolean valued approach. $\endgroup$ – Mohammad Golshani Jun 29 '20 at 16:59
  • $\begingroup$ Thanks @MohammadGolshani for your clarification. Also, I do not know if classical realizability fits in any of those four approaches. In any case, I'd be interested in knowing if my claim that the first two are the main ones is incorrect. $\endgroup$ – Pedro Sánchez Terraf Jun 29 '20 at 19:08

There are two types of "working with forcing":

  1. We can develop the theory of forcing, e.g. iterations, where working with canonical forcing notions is somewhat preferable, so dealing with complete Boolean algebras is somehow the most natural approach, and by extension with Boolean-valued models (well, sometimes).

    For example, talking about homogeneity conditions is easy when you have them. But maybe you have a rigid partial order which is forcing equivalent to adding a Cohen real (e.g. construct a tree where each node has a unique number of successors). Or perhaps you want to iterate forcings, but the standard definition of iteration given in terms of partial orders is a pre-ordered set. Being able to forego all of that and just find an invariant is great.

  2. We can use the theory of forcing, e.g. proving various consistency results. In this case it is almost exclusively done with partial orders, and indeed with pre-orders, where we simply ignore all of the forcing theoretic issues that make the "formally correct statements" just a huge pain in the lower-lower-back to state.

    I think this is best reflected in Jech's "Set Theory" book (3rd edition, for those keeping track). The basic theory of forcing is developed with Boolean algebras and Boolean-valued models. When forcing is actually used, Jech quickly reverts back to partial orders and pre-orders, instead.

Now you can also talk about forcing with topological spaces, forcing with sheaves (or shivs), etc. This is not very common in set theoretic papers in the last few decades. I won't comment on other subjects, as I'm not an expert.

Finally, a word about the foundations of forcing. When one learns about forcing, it is often confusing. The generic object is seemingly black magic, and what's going on with those Cohen reals encoded in limit steps? And what is this "arbitrarily large, but finite fragment of $\sf ZFC$" that Kunen keeps talking about?

Well, the reality is that we can develop forcing in a lot of different ways:

  1. Just force over countable transitive models of $\sf ZFC$. That's the simplest, most straightforward way to do it. But this requires us to assume more in terms of consistency.

  2. Just force over countable models of $\sf ZFC$. Oh, but then it gets ugly when talking about things like ordinals and whatnot, because these models are not necessarily well-founded. Also, this requires more consistency, although significantly less than before.

  3. Use reflection to argue that we can find countable transitive models of any large enough fragment of $\sf ZFC$, force over those, and use a meta-theoretic argument to conclude the proof.

  4. Use Boolean-valued models to develop forcing as a proper class and argue with Boolean-valued truth that certain statement are consistent. But that's kind of yuck in most cases.

  5. Instead of Boolean-valued models, define an "internal ultrapower" of the universe by extending the filter base that is the dense open sets to a "generic" filter, and use this model, where the forcing theorem and truth lemma still hold, to finish your argument. In some sense this is a neater version of Boolean-valued models, but in another sense it is quite the opposite.

  6. Use Feferman's theory, where we add a constant symbol, postulate that it is a countable transitive elementary submodel of the universe, then force over that model. No additional consistency is needed, as Feferman's theory is finitely consistent (assuming $\sf ZFC$ is), so it is given to us. But it sort of makes this specified model somehow... on a pedestal. Also without further assumptions (which are tantamount to (1) with more power) the models of Feferman's theory are ill-founded, which is yuck to think about from a meta-theoretic point of view.

  7. Use other tricks and machinery to encode forcing and just work syntactically in a theory as weak as $\sf PRA$. (Shudder here.)

But what do people actually end up doing (once they grok forcing)? Well. We force over the universe. We just ignore all of it and force over the universe. Because at the end of the day, the goal is to use forcing, and as all of these approaches lead us to the same way, and we anyway define everything and work internally to whatever set-sized model we may have used, we might as well force over the universe. Simply rub your hands, and a generic appears! Magic!

  • $\begingroup$ Thank you very much Asaf. It was confusing for me, and when first reading Jech I did wonder where the heck did $G$ come from. With Kunen I felt reassured, and by jumping inside a ctm, I was able to understand what it felt to have a generic visit from outer space. Now, when you force over $V$, do you feel the same :-)? Which of the approaches represents that feeling better? $\endgroup$ – Pedro Sánchez Terraf Jun 29 '20 at 20:55
  • 2
    $\begingroup$ Hey, as long as people are reading my papers... :-) $\endgroup$ – Asaf Karagila Jun 29 '20 at 21:53
  • 2
    $\begingroup$ It remains an interesting practical question what approach a proof assistant should take. Requiring additional consistency is probably undesirable and PRA is horrible. People use partial orders in practice so BVMs seem awkward. I don't know how easily proof assistants can implement the meta-theoretic argument of your option 3. So maybe 5 or 6 is the way to go? $\endgroup$ – Timothy Chow Jun 30 '20 at 21:36
  • 1
    $\begingroup$ @AsafKaragila : I don't think proof assistants are necessarily "wired to be syntactic" in this particular sense; on the other hand, from the point of view of, say, reverse mathematics, it's valuable to know that some of these theorems can be proved in very weak systems. Here's a question: How often in practice do set theorists need the fact that some theorem (proved using forcing) is provable in some system that is much weaker than ZF? My impression is that this is rare. One just declares that one is working in ZF and it never matters that some weaker system suffices. $\endgroup$ – Timothy Chow Jul 1 '20 at 18:30
  • 2
    $\begingroup$ @PedroSánchezTerraf: One can argue that meta-reasoning is in fact "the reasoning", because we are proving a theorem about ZFC, rather than proving a theorem in ZFC. Forcing is just useful this way that it lets you work from within a model within the theory, without worrying about the theory itself. $\endgroup$ – Asaf Karagila Jul 3 '20 at 13:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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