Which is the more popular approach to forcing in the literature?

Question

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.

Answer 1

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!