6
$\begingroup$

The set-theoretical notion of forcing is based on a poset $\mathbb{P}$ (the forcing notion) that allows us to define suitable names of elements we want to appear in the forcing extension of our ground model. Using those names, we may even define sentences in the forcing language. The forcing theorem ties these notions together, and turns sentences in the forcing language into sentences in the language of set theory (i.e. get rid of names, since names turn into elements in the extension). Crucially, conditions force sentences in this language.

In computability theory, however, we have a definition of the following form: considering Cohen forcing, a real $f \in 2^{\omega}$ (i.e. a generic, basically a filter) forces a set $V_e \subset 2^{< \omega}$ of finite strings iff $$ \exists \sigma \prec f ( \sigma \in V_e \lor \forall \rho \succ \sigma (\rho \not\in V_e)) $$ which is also called the forcing requirement. (Here $\sigma \prec f$ means $\sigma$ is a proper initial segment of $f$.)

I see how this definition of forcing aligns with the set-theoretical one (in set-theoretical forcing, $M[G] \vDash \psi$ only if there is a condition $p \in G$ that forces it, and if $p \in G$ but no extension $q \leq p$ forces the negation, the result follows), I think?

But mostly I'm confused about the following: $V_e$ is a set of finite strings; in particular, it is not a statement in any language. So, what does it intuitively mean to "force a set"?

$\endgroup$
3
  • $\begingroup$ Where did you find this meaning for "$f$ forces $V_e$"? It looks very strange to me; I'd rather use terminology like "$f$(or $\sigma$) decides $V_e$." $\endgroup$ May 8, 2020 at 16:22
  • 1
    $\begingroup$ @AndreasBlass This is sadly common in my experience (see e.g. "forces the jump"). It tripped me up a lot when learning the topic initially, FWIW. $\endgroup$ May 8, 2020 at 16:26
  • $\begingroup$ @NoahSchweber Thanks. $\endgroup$ May 8, 2020 at 16:30

1 Answer 1

4
$\begingroup$

There are a couple tricks of language being used here:

  • First, we conflate $V\subseteq 2^\omega$ with the corresponding forcing sentence "The generic is an element of $V$."

  • Second, we talk about a real $f\in 2^\omega$ forcing some sentence $\varphi$ if some condition $\sigma\prec f$ either forces $\varphi$ or forces $\neg\varphi$ in the classical sense.

    • So really that's two conflations: juggling between filters and conditions, and using "forces" instead of something more even-handed like "decides."

So "$f$ forces $V$" means "There is some condition $\sigma\prec f$ such that either $\sigma\Vdash\dot{f}\in V$ or $\sigma\Vdash\dot{f}\not\in V$" (where I'm using "$\dot{f}$" to denote the canonical name for the generic object). In my opinion a better, if somewhat more clunky, phrasing would be:

For $f$, "forcing = truth" as far as membership in $V$ goes.

There are broadly speaking two ways of phrasing "somewhat-genericity" which show up computability theory: meeting lots of dense sets, and having "forcing = truth" for lots of sentences. Note that the relationship between these phrasings is a bit more nuanced than one might expect: "meets every dense c.e. set" is slightly weaker than "meets or avoids from every c.e. set," and only the latter gives us "forcing = truth" for $\Sigma^0_1$ sentences. (Here by "avoids" I mean the strong sense: $f\in 2^\omega$ avoids $W\subseteq 2^\omega$ if there is some $\sigma\prec f$ such that no $\tau$ compatible with $\sigma$ lies in $W$.)


As a coda, let me observe that there's an interesting cultural divide here, incidentally: in my experience most computability theorists are more comfortable with properties of the form "meets every dense set of complexity $\Gamma$" than with properties of the form "has "forcing = truth" for every sentence of complexity $\Delta$." By contrast, I ran into set-theoretic forcing before really seeing much computability-theoretic forcing, and so for me it's more natural to talk about "forcing = truth." Based on your question it sounds like you're more familiar at the moment with set-theoretic forcing than with computability-theoretic forcing, so I suspect you'll have the same experience.

$\endgroup$
4
  • 1
    $\begingroup$ Your coda sounds like you've found a disciple. Or perhaps a master-apprentice situation, Darth Schwebious. $\endgroup$
    – Asaf Karagila
    May 8, 2020 at 17:29
  • $\begingroup$ Thank you Noah -- I certainly am more comfortable with set-theoretical forcing, no doubt! Could you clarify this for more perhaps: how does one see that meeting or avoiding every c.e. set is the same as deciding a $\Sigma_1^0$ sentence? The c.e. sets are, by definition, exactly the $\Sigma_1^0$-sets, but I understand from the first part of your answer that such a $\Sigma_1^0$ sentence is just of the form "$f \in V$" where $V$ is the c.e. set in question. Is that correct? $\endgroup$
    – MacRance
    May 8, 2020 at 23:04
  • 1
    $\begingroup$ @MacRance: Just to clarify, computability is the dark side of the forcing. But you're there now, Darth Rancious. $\endgroup$
    – Asaf Karagila
    May 9, 2020 at 0:47
  • $\begingroup$ @AsafKaragila I'm trying to stick to the (so much) greener pastures of set theory -- after this post I'm on my way back, don't worry ;) $\endgroup$
    – MacRance
    May 9, 2020 at 6:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .