Jump to content

Forcing (computability)

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Peter M Gerdes (talk | contribs) at 12:03, 15 September 2007 (Got started...I'll come back and leave it less half-finished later). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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

Terminology and General Remarks

In this article we use the following terminology (standard in the field). A realis an element of . In other words a function that maps each integer to either 0 or 1. A string is an element of . In other words a finite approximation to a real.

Definition of Forcing

We now define the basic notions

notion of forcing
A notion of forcing is a set and a partial order on , with a greatest element .
is stronger than
Given for a notion of forcing we say that is stronger than when . Note that this means that will usually turn out to be the reverse of the containment relation. Be careful some recursion theorists reverse the direction of which seems more natural in many recursion theoretic contexts but is at odds with the notation used in set theory.


Technically as in set theoretic forcing the result of a forcing construction will be an ultrafilter on . That is we will produce a set of conditions so that if then there is an so that