Forcing (computability)

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 ${\displaystyle ⊩}$) 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 ${\displaystyle 2^{\omega }}$. In other words, a function that maps each integer to either 0 or 1.

string

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

notion of forcing

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

condition

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

compatible conditions

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

${\displaystyle p\mid q}$

means ${\displaystyle p}$ and ${\displaystyle q}$ are incompatible.

Filter

A subset ${\displaystyle F}$ of a notion of forcing ${\displaystyle P}$ is a filter if ${\displaystyle p,q\in F⟹p\nmid q}$, and ${\displaystyle p\in F\wedge q{\succ }_{P}p⟹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., ${\displaystyle F}$ is an ultrafilter if ${\displaystyle F}$ is a filter and there is no filter ${\displaystyle F^{\prime }}$ properly containing ${\displaystyle F}$.

Cohen forcing

The notion of forcing ${\displaystyle C}$ where conditions are elements of ${\displaystyle 2^{<\omega }}$ and ${\displaystyle (\tau {\succ }_C\sigma ⟺\sigma \supset \tau }$)

Note that for Cohen forcing ${\displaystyle {\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 ${\displaystyle {\succ }_P}$ with ${\displaystyle {\prec }_P}$, which is more natural for Cohen forcing, but is at odds with the notation used in set theory).