Paul Cohen on genesis of method of forcing and mathematical similarities

Question

We have on record Paul Cohen's comments on being inspired by issues of formalizing algorithms in number theory (this needs to be verified as per comment) as well as related remarks on computability. Beyond such "inspiration", are there mathematical similarities between developments in those fields and Cohen's work on forcing? A related question was posed at MSE with limited success.

Answer 1

(This was written a bit hastily, so apologies for any errors/omissions.)

The answers by Ali Enayat and I to a related MO question address the broad connections between forcing and techniques in computability theory which emerged over time (that is, without claiming anything about their impact on Cohen re: the discovery of forcing). In particular, at that question I argue that while there is a clear analogy between finite extension arguments and forcing, there is also a less clear analogy between forcing axioms and priority arguments. I think regardless of whether Cohen was consciously thinking of computability theory per se when he invented forcing, the connections between forcing arguments and many kinds of computability-theoretic constructions are deep and fundamental, and I also believe that this opinion is broadly held amongst logicians. (Note that this is not the same as saying that undecidability proofs are at all connected with forcing, and indeed I don't think they are except possibly in rare cases; I'll update my answer to your other question to clarify this soon.)

Another more specific similarity between forcing and computability theory is evident in the theory of effective cardinal characteristics of the continuum, where the classical forcing arguments proving consistent separation can often be converted into arguments showing an unconditional result onthe computability-theoretic side (and there are natural variations on the specific framework for effective cccs which have largely been unexplored; see this paper of Kihara for a rare exception, where "effective" is replaced with "hyperarithmetic" yielding intriguing differences).

As far as other areas of logic go, in proof theory there are connections with intuitionistic and modal logic, and forcing notions in model theory have proved important, but I'm not qualified to say much about these.

And of course I'm not qualified at all to talk about the connections with number theory, but it's worth pointing out that there are results severly limiting the direct relevance of forcing (and similar techniques) to number theory; meanwhile, intuitively speaking any specific natural number is specified by "finitely many decisions," while forcing is only interesting when we're making "infinitely many decisions," so I don't see how forcing could be used to produce interesting examples of number-theoretic phenomena at the number level. However, arguments producing sets of natural numbers with certain properties can be thought of as having "forcing flavor" - e.g. the construction of a set whose upper and lower densities are different can be thought of as "baby" Cohen forcing - but this is really Baire category flavor, rather than forcing per se. So I would be very surprised if Cohen's intuitive analogy ever bore fruit in the form of real results.

---

Now I'll depart from your actual question. I hope you find this relevant; if not, let me know and I'll delete it.

You don't explicitly ask for this, but I think it's worth mentioning that the closest mathematical relative of forcing is from topology: it's the Baire category theorem. Take a countable model $M\models ZF$ and a poset $\mathbb{P}\in M$. The collection of maximal filters through $\mathbb{P}$ has a natural topology, where the basic open sets are generated by elements of $\mathbb{P}$ in the usual way; call this space "$\mathcal{F}_\mathbb{P}$." There are of course only countably many dense open subsets of this space in $M$, so there are $\mathbb{P}$-generic filters over $M$. This is the Rasiowa-Sikorski lemma, but its proof is exactly the same as the proof of the Baire category theorem for the Baire space $\omega^\omega$ (the proof of BCT for $\mathbb{R}$ which uses local compactness of course does not work here).

Where forcing goes beyond the spirit of BCT, then, is in the analysis of these generic filters, and in particular the following three observations:

• The inductive notion of names lets us go from the model $M$ together with the generic $G$ to a new structure $M[G]$ in the language of set theory. (This is straightforward if $M$ is well-founded; if $M$ is not well-founded, it takes a bit more thought but still works.) This is very special to set theory. In general, we can make sense of forcing over pretty much arbitrary countable structures using posets which "live" in those structures appropriately, but the result is a structure in a new language - the original language together with a predicate symbol (or symbols) describing the generic filter. "Typed" structures have the nice property that the generic through poset whose elements have "small" type can be represented by a single object of "large" type; models of ZF aren't literally typed, of course, but their hierarchical structure does the job. It's also of course essential that $M[G]\models$ZF (and ZFC if $M$ satisfied ZFC); a priori, we might not expect this to be true, and it doesn't always hold if we replace ZF with fragments of ZF. Further, the names themselves admit structural analyses, letting us define interesting intermediate objects - "symmetric submodels" of $M[G]$.

(Incidentally, the "predicate picture" comes back when we look at class forcing, but that's a much less fundamental technique, at least so far.)

• Properties of the structure $M[G]$ are determined by the elements of $G$: for every $\varphi$, if $G$ is generic then exactly one of the following holds: either there is some $p\in G$ such that for every $\mathbb{P}$-generic filter $H$ over $M$ which contains $p$, we have $M[H]\models\varphi$, or there is some $p\in G$ such that for every $\mathbb{P}$-generic filter $H$ over $M$ which contains $p$, we have $M[H]\models\neg\varphi$. This is proved by induction on the complexity of $\varphi$; we can cook up analogous topological analogues, but I've never seen these used outside of set theory.

• The forcing relation is in fact definable in $M$, even though a priori it is only expressed externally. This definability is crucial to the method: it lets us verify that $M[G]$ has certain properties by allowing us to construct in $M$ names which witness those properties appropriately, by means of the definition in $M$ of the forcing relation. For example, to show that $\mathbb{R}^{M[G]}=\mathbb{R}^M$ if $\mathbb{P}$ is countably closed (which is crucial to forcing CH), we find for each name $\nu$ for a real a condition $p$ such that for each $i\in\omega$ there is some $j_i\in\omega$ with $p\Vdash \nu(i)=j_i$; we then use the definability of the forcing relation to show that the real $i\mapsto j_i$ is in fact in $M$. In more complicated arguments we may "ping-pong" between $M$ and $M[G]$ in more intricate ways.

For me, the way in which these three aspects occur in set-theoretic forcing makes it fundamentally unique amongst all mathematical techniques I'm aware of, notwithstanding its partial connections to other techniques of variable meaningfulness.

Answer 2

Regarding your question about the connection between forcing and computability theory, the notion of a Cohen generic oracle is used in computational complexity; see for example An oracle builder's toolkit by Fenner et al. For a different kind of connection, see Chapter 13 ("Forcing and Category") of S. Barry Cooper's book Computability Theory (unfortunately I don't think that the complete text is available online).

As for the connection to arithmetic, see Forcing over set theory versus forcing over arithmetic