Forcing (computability): Difference between revisions

Revision as of 20:00, 14 February 2011

Latest revision as of 03:06, 4 June 2025

(21 intermediate revisions by 13 users not shown)

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

'''Forcing''' in [[computability 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 computability concerns.

'''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 setsset]]s. Also bothBoth 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 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 recursion theorycomputability. But while the machinery may be somewhat different, recursion 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 <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. 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\midcompatible q</math> (<math>p</math> incompatible with <math>q</math>)conditions: Given conditions <math>p,q</math> say that <math>p</math> and <math>q</math> are incompatible (denoted <math>p\mid q</math>)compatible if there is noa condition <math>r</math> withsuch <math>that pwith \succ_Prespect r</math> andto <math>q \succ_P r</math>., both <math>p</math> is compatible withand <math>q</math> can be simultaneously satisfied if they are nottrue incompatible.or allowed to coexist.<!-- Sometimes we will use '''consistent''' as a synonym for compatible. -->

;<math>p\mid q</math>

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

means <math>p</math> and <math>q</math> are incompatible.

;UltrafilterFilter : A maximal filter, i.e.,subset <math>F</math> isof ana ultrafilternotion ifof forcing <math>FP</math> is a filter andif there<math>p,q is\in noF filter\implies <math>F'p \nmid q</math>, properly containingand <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.

; Cohen forcingUltrafilter: TheA notionmaximal offilter, forcingi.e., <math>CF</math> whereis conditionsan areultrafilter elements ofif <math>(2^{<\omega}F</math> is a filter and <math>\tauthere \succ_Cis \sigmano \ifffilter \sigma<math>F'</math> \supsetproperly \taucontaining <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 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 ==

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

== Forcing relation ==

The forcing relation <math>\Vdash</math> was developed by [[Paul Cohen]], who introduced forcing as a technique for proving the independence of certain statements from the standard axioms of set theory, particularly the [[continuum hypothesis]] (CH).

The notation <math>V \Vdash \phi</math> is used to express that a particular condition or generic set forces a certain proposition or formula <math>\phi</math> to be true in the resulting forcing extension. Here's <math>V</math> represents the original universe of sets (the ground model), <math>\Vdash</math> denotes the forcing relation, and <math>\phi</math> is a statement in set theory.

When <math>V \Vdash \phi</math>, it means that in a suitable forcing extension, the statement <math>\phi</math> will be true.

== References ==

*{{Cite book

* Melvin Fitting (1981), ''Fundamentals of generalized recursion theory''.

|last=Fitting

* Piergiorgio Odifreddi (1999), ''Classical Recursion Theory'', v. 2.

|first=Melvin

|author-link=Melvin Fitting

|year=1981

* Melvin Fitting (1981), ''|title=Fundamentals of generalized recursion theory''.

|publisher=North-Holland Publishing Company

|___location=Amsterdam, New York, and Oxford

|series=Studies in Logic and the Foundations of Mathematics

|pages=1078–1079

|doi=10.2307/2273928

|volume=105

|jstor=2273928

|s2cid=118376273

}}

*{{Cite book

|last=Odifreddi

|first=Piergiorgio

|author-link=Piergiorgio Odifreddi

|year=1999

|title=Classical recursion theory. Vol. II

|publisher=North-Holland Publishing Company

|___location=Amsterdam

|series=Studies in Logic and the Foundations of Mathematics

|isbn=978-0-444-50205-6

|mr=1718169

|volume=143

}}

[[Category:Computability theory]]