Forcing (computability)

Forcing in recursion theory is a modification of Paul Cohen's original set theoretic technique of forcing to deal with the effective concerns in recursion theory. 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. Also both techniques are elegantly 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, recursion 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 eliminate or substantially simplified when defining forcing in recursion theory. But while the machinery may be somewhat different recursion theoretic and set theoretic forcing are properly regarded as an application of the same technique to different classes of formulas.

Definition of Forcing

Basic 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.

Cohen forcing

The notion of forcing $C$ where conditions are elements of $(2^{<\omega }$ and $\tau \succ _{C}\sigma \iff \sigma \supset \tau$

Given $\sigma ,\tau \in P$ for a notion of forcing $P$ we say that $\sigma$ is stronger than $\tau$ when $\tau \succ _{P}\sigma$. Note that this means that $\succ _{P}$ will usually turn out to be the reverse of the containment relation. Be careful some recursion theorists reverse the direction of $\succ _{P}$ which seems more natural in many recursion theoretic contexts but is at odds with the notation used in set theory.

The intuition here 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 it's own.

Language of Forcing

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 (mathematics) 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.