Forcing (computability): Difference between revisions

Revision as of 00:34, 26 April 2021

Revision as of 00:37, 26 April 2021

Line 1:

'''Forcing''' in [[recursioncomputability theory]] is a modification of [[Paul Cohen (mathematician)|Paul Cohen's]] original [[set theory|set-theoretic]] technique of [[forcing (set theory)|forcing]] to deal with the effectivecomputability concerns in [[recursion theory]].

Conceptually the two techniques are quite similar: in both one attempts to build [[generic set|generic]] objects (intuitively objects that are somehow 'typical') by meeting dense sets. Both techniques are described as a relation (customarily denoted <math>\Vdash</math>) 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, recursioncomputability-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 recursion theorycomputability. But while the machinery may be somewhat different, recursioncomputability-theoretic and set-theoretic forcing are properly regarded as an application of the same technique to different classes of formulas.

==Terminology==

Line 23 ⟶ 25:

;Cohen forcing: The notion of forcing <math>C</math> where conditions are elements of <math>2^{<\omega}</math> and <math>(\tau \succ_C \sigma \iff \sigma \supset \tau</math>)

Note that for Cohen forcing <math>\succ_{C}</math> is the '''reverse''' of the containment relation. This leads to an unfortunate notational confusion where some recursioncomputability theorists reverse the direction of the forcing partial order (exchanging <math>\succ_P</math> with <math>\prec_P</math>, which is more natural for Cohen forcing, but is at odds with the notation used in set theory).

== Generic objects ==