Forcing (computability): Difference between revisions

Revision as of 04:56, 11 January 2008

Latest revision as of 03:06, 4 June 2025

(29 intermediate revisions by 17 users not shown)

Line 1:

{{references|date=January 2008}}

'''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 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 cohenCohen 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 ==

{{mathlogic-stub}}

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

[[Category:Recursion theory]]

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

|last=Fitting

|first=Melvin

|author-link=Melvin Fitting

|year=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:RecursionComputability theory]]