Forcing (computability): Difference between revisions

Revision as of 12:26, 7 March 2018

Revision as of 16:25, 13 October 2019

Line 1:

'''Forcing''' in [[recursion 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 effective 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 elegantly 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, recursion -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 theory. But while the machinery may be somewhat different, recursion -theoretic and set -theoretic forcing are properly regarded as an application of the same technique to different classes of formulas.

==Terminology==

Line 14:

;compatible conditions: Given conditions <math>p,q</math> say that <math>p</math> and <math>q</math> are compatible if there is a condition <math>r</math> with <math> p \succ_P r</math> and <math>q \succ_P r</math>. <!-- Sometimes we will use '''consistent''' as a synonym for compatible. -->

;<math>p\mid q</math>:
means <math>p</math> and <math>q</math> are incompatible.

;Filter : A subset <math>F</math> of a notion of forcing <math>P</math> is a filter if <math>p,q \in F \implies p \nmid q</math>, and <math>p \in F \land q \succ_P p \implies q \in F</math>. In other words, a filter is a compatible set of conditions closed under weakening of conditions.

;Ultrafilter: A maximal filter, i.e., <math>F</math> is an ultrafilter if <math>F</math> is a filter and there is no filter <math>F'</math> properly containing <math>F</math>.

;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 recursion 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 ==

The intuition behind forcing is that our conditions are finite approximations to some object we wish to build and that <math>\sigma</math> is stronger than <math>\tau</math> when <math>\sigma</math> agrees with everything <math>\tau</math> 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 <math>\tau \succ_C \sigma</math> then <math>\sigma</math> tells us the value of the real onat more places.

In a moment we will define a relation <math>\sigma \Vdash_P \psi</math> (read <math>\sigma</math> forces <math>\psi</math>) that holds between conditions (elements of <math>P</math>) and sentences, but first we need to explain the [[language (mathematics)|langugae]] that <math>\psi</math> is a sentence for. However, forcing is a technique, not a definition, and the language for <math>\psi</math> will depend on the application one has in mind and the choice of <math>P</math>.

The idea is that our language should express facts about the object we wish to build with our forcing construction.