Forcing in computability theory is a modification of Paul Cohen's original set-theoretic technique of forcing to deal with computability concerns.
| This article needs attention from an expert in mathematics or logic. The specific problem is: Article incomplete. (April 2021) |
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.
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 such that with respect to , both and can be simultaneously satisfied if they are true or allowed to coexist.
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).