Forcing (computability): Difference between revisions

Revision as of 16:07, 21 October 2019

Latest revision as of 03:06, 4 June 2025

(13 intermediate revisions by 7 users not shown)

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

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 set]]s. 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 13 ⟶ 15:

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

;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> such that with respect to <math>r</math>, pboth \succ_P r<math>p</math> and <math>q \succ_P r</math>. can be simultaneously satisfied if they are true or allowed to coexist.<!-- Sometimes we will use '''consistent''' as a synonym for compatible. -->

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

Line 24 ⟶ 26:

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

Line 30 ⟶ 32:

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 at 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)|langugaelanguage]] 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]]