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 formula_1) 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.
means formula_8 and formula_9 are incompatible.
Note that for Cohen forcing formula_32 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 formula_33 with formula_34, 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 formula_35 is stronger than formula_36 when formula_35 agrees with everything formula_36 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 formula_39 then formula_35 tells us the value of the real at more places.
In a moment we will define a relation formula_41 (read formula_35 forces formula_43) that holds between conditions (elements of formula_4) and sentences, but first we need to explain the language that formula_43 is a sentence for. However, forcing is a technique, not a definition, and the language for formula_43 will depend on the application one has in mind and the choice of formula_4.
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 formula_1 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 formula_49 is used to express that a particular condition or generic set forces a certain proposition or formula formula_50 to be true in the resulting forcing extension. Here's formula_51 represents the original universe of sets (the ground model), formula_1 denotes the forcing relation, and formula_50 is a statement in set theory.
When formula_49, it means that in a suitable forcing extension, the statement formula_50 will be true.