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"?
Best Answer
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 "$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:
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.