Forcing (computability): Difference between revisions

Revision as of 12:26, 15 September 2007

Revision as of 17:18, 23 September 2007

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. Also 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 eliminate 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.

==Motivation==

== Definition of Forcing ==

===Basic Terminology===

Stuff goes here about why we want to use forcing.

===Basic Terminology===

In this article we use the following terminology.

Line 8 ⟶ 11:

;real: an element of <math>2^\omega</math>. In other words a function that maps each integer to either 0 or 1.

;string: an element of <math>2^{<\omega}</math>. In other words a finite approximation to a real.

; notion of forcing : A notion of forcing is a set <math>P</math> and a [[partial order]] on <math>P</math>, <math>\succ_{P}</math> with a ''greatest element'' <math>0_{P}</math>.

;condition: An element in a notion of forcing.

;condition: An element in a notion of forcing. We say a condition <math>p</math> is stronger than a condition <math>q</math> just when <math>q \succ_P p</math>.

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

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

GivenNote <math>\sigma,\tau \in P</math>that for a notion ofcohen forcing <math>P</math> we say that <math>\sigma</math> is stronger than <math>\tau</math> when <math>\tau \succ_P \sigma</math>. Note that this means that <math>\succ_{PC}</math> will usually turn out to beis the '''reverse''' of the containment relation. '''BeThis leads to an unfortunate notational confusion carefulwhere some recursion theorists reverse the direction of the forcing partial order (exchanging <math>\succ_P</math>''' with <math>\prec_P</math> which seemsis more natural infor manyCohen recursion theoretic contextsforcing but is at odds with the notation used in set theory.

== Generic Objects ==

The intuition herebehind 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 it's 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 on more places.

Theoretically one could view any forcing argument as the construction of an [[ultrafilter]] with special properties, that is a maximal compatible subset of

The intuition here 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 it's own.

===Language of Forcing===

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)]] 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>.