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

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 \Vdash ) 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 2^\omega . In other words, a function that maps each integer to either 0 or 1. string: an element of 2^{ . In other words, a finite approximation to a real. notion of forcing: A notion of forcing is a set P and a partial order on P , \succ_{P} with a greatest element 0_{P} . condition: An element in a notion of forcing. We say a condition p is stronger than a condition q just when q \succ_P p . compatible conditions: Given conditions p,q say that p and q are compatible if there is a condition r such that with respect to r , both p and q can be simultaneously satisfied if they are true or allowed to coexist. p\mid q means p and q are incompatible. Filter : A subset F of a notion of forcing P is a filter if p,q \in F \implies p \nmid q , and 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., F is an ultrafilter if F is a filter and there is no filter F' properly containing F . Cohen forcing: The notion of forcing C where conditions are elements of 2^{ and (\tau \succ_C \sigma \iff \sigma \supset \tau ) Note that for Cohen forcing \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 \succ_P with \prec_P , which is more natural for Cohen forcing, but is at odds with the notation used in set theory).

Text derived from https://en.wikipedia.org/w/index.php?oldid=1345549008 under CC BY-SA 4.0; modifications have been made.