# Forcing (computability)

Forcing in computability theory is a modification of Paul Cohen's original set-theoretic technique of forcing to deal with computability concerns.
Conceptually the two techniques are quite similar: in both one attempts to build generic objects (intuitively objects that are somehow 'typical') by meeting dense sets. Both techniques are described as a relation (customarily denoted $\Vdash$) between 'conditions' and sentences. However, where set-theoretic forcing is usually interested in creating objects that meet every dense set of conditions in the ground model, computability-theoretic forcing only aims to meet dense sets that are arithmetically or hyperarithmetically definable. Therefore, some of the more difficult machinery used in set-theoretic forcing can be eliminated or substantially simplified when defining forcing in computability. But while the machinery may be somewhat different, computability-theoretic and set-theoretic forcing are properly regarded as an application of the same technique to different classes of formulas.

## Terminology

In this article we use the following terminology.

### real

    an element of $2^{\omega }$. In other words, a function that maps each integer to either 0 or 1.

### string

    an element of $2^{<\omega }$. In other words, a finite approximation to a real.

### notion of forcing

    A notion of forcing is a set $P$ and a partial order on $P$, $\succ _{P}$ with a greatest element $0_{P}$.

### condition

    An element in a notion of forcing. We say a condition $p$ is stronger than a condition $q$ just when $q\succ _{P}p$.

### compatible conditions

    Given conditions $p,q$ say that $p$ and $q$ are compatible if there is a condition $r$ such that with respect to $r$, both $p$ and $q$ can be simultaneously satisfied if they are true or allowed to coexist.

### $p\mid q$

means $p$ and $q$ are incompatible.

### Filter

    A subset $F$ of a notion of forcing $P$ is a filter if $p,q\in F\implies p\nmid q$, and $p\in F\land q\succ _{P}p\implies q\in F$. In other words, a filter is a compatible set of conditions closed under weakening of conditions.

### Ultrafilter

    A maximal filter, i.e., $F$ is an ultrafilter if $F$ is a filter and there is no filter $F'$ properly containing $F$.

### Cohen forcing

    The notion of forcing $C$ where conditions are elements of $2^{<\omega }$ and $(\tau \succ _{C}\sigma \iff \sigma \supset \tau$)
Note that for Cohen forcing $\succ _{C}$ is the reverse of the containment relation. This leads to an unfortunate notational confusion where some computability theorists reverse the direction of the forcing partial order (exchanging $\succ _{P}$ with $\prec _{P}$, which is more natural for Cohen forcing, but is at odds with the notation used in set theory).

## Generic objects

The intuition behind forcing is that our conditions are finite approximations to some object we wish to build and that $\sigma$ is stronger than $\tau$ when $\sigma$ agrees with everything $\tau$ says about the object we are building and adds some information of its own. For instance in Cohen forcing the conditions can be viewed as finite approximations to a real and if $\tau \succ _{C}\sigma$ then $\sigma$ tells us the value of the real at more places.
In a moment we will define a relation $\sigma \Vdash _{P}\psi$ (read $\sigma$ forces $\psi$) that holds between conditions (elements of $P$) and sentences, but first we need to explain the language that $\psi$ is a sentence for. However, forcing is a technique, not a definition, and the language for $\psi$ will depend on the application one has in mind and the choice of $P$.
The idea is that our language should express facts about the object we wish to build with our forcing construction.

## Forcing relation

The forcing relation $\Vdash$ was developed by Paul Cohen, who introduced forcing as a technique for proving the independence of certain statements from the standard axioms of set theory, particularly the continuum hypothesis (CH).
The notation $V\Vdash \phi$ is used to express that a particular condition or generic set forces a certain proposition or formula $\phi$ to be true in the resulting forcing extension. Here's $V$ represents the original universe of sets (the ground model), $\Vdash$ denotes the forcing relation, and $\phi$ is a statement in set theory. When $V\Vdash \phi$, it means that in a suitable forcing extension, the statement $\phi$ will be true.