Forcing (computability)

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}$ with ${\displaystyle p\succ _{P}r}$ and ${\displaystyle q\succ _{P}r}$.

${\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\implies p\nmid q}$, and ${\displaystyle 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., ${\displaystyle F}$ is an ultrafilter if ${\displaystyle F}$ is a filter and there is no filter ${\displaystyle F'}$ 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 \iff \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).

The intuition behind forcing is that our conditions are finite approximations to some object we wish to build and that ${\displaystyle \sigma }$ is stronger than ${\displaystyle \tau }$ when ${\displaystyle \sigma }$ agrees with everything ${\displaystyle \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 ${\displaystyle \tau \succ _{C}\sigma }$ then ${\displaystyle \sigma }$ tells us the value of the real at more places.

In a moment we will define a relation ${\displaystyle \sigma \Vdash _{P}\psi }$ (read ${\displaystyle \sigma }$ forces ${\displaystyle \psi }$) that holds between conditions (elements of ${\displaystyle P}$) and sentences, but first we need to explain the language that ${\displaystyle \psi }$ is a sentence for. However, forcing is a technique, not a definition, and the language for ${\displaystyle \psi }$ will depend on the application one has in mind and the choice of ${\displaystyle P}$.

The idea is that our language should express facts about the object we wish to build with our forcing construction.

• Fitting, Melvin (1981). Fundamentals of generalized recursion theory. Studies in Logic and the Foundations of Mathematics. Vol. 105. Amsterdam, New York, and Oxford: North-Holland Publishing Company. pp. 1078–1079. doi:10.2307/2273928.
• Odifreddi, Piergiorgio (1999). Classical recursion theory. Vol. II. Studies in Logic and the Foundations of Mathematics. Vol. 143. Amsterdam: North-Holland Publishing Company. ISBN 978-0-444-50205-6. MR 1718169.