Forcing (computability)
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 ) 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 . In other words, a function that maps each integer to either 0 or 1. 
string  an element of . In other words, a finite approximation to a real. notion of forcing A notion of forcing is a set  and a partial order on ,  with a greatest element . condition An element in a notion of forcing. We say a condition  is stronger than a condition  just when . compatible conditions Given conditions  say that  and  are compatible if there is a condition  with  and . means  and  are incompatible. Filter  A subset  of a notion of forcing  is a filter if , and . In other words, a filter is a compatible set of conditions closed under weakening of conditions. Ultrafilter A maximal filter, i.e.,  is an ultrafilter if  is a filter and there is no filter  properly containing . Cohen forcing The notion of forcing  where conditions are elements of  and )

Note that for Cohen forcing  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  with ,  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  is stronger than  when  agrees with everything  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  then  tells us the value of the real at more places. In a moment we will define a relation  (read  forces ) that holds between conditions (elements of ) and sentences, but first we need to explain the language that  is a sentence for. However, forcing is a technique, not a definition, and the language for  will depend on the application one has in mind and the choice of . The idea is that our language should express facts about the object we wish to build with our forcing construction. References 

Computability theory