Forcing (computability)

Forcing in computability theory is a modification of Paul Cohen's original set-theoretic technique of forcing to deal with computability concerns.

Conceptually the two techniques are quite similar: in both one attempts to build generic objects (intuitively objects that are somehow 'typical') by meeting dense sets. Both techniques are described as a relation (customarily denoted [math]\displaystyle{ \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, 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 computability. But while the machinery may be somewhat different, computability-theoretic and set-theoretic forcing are properly regarded as an application of the same technique to different classes of formulas.

## Contents

* 1 Terminology
* 2 Generic objects
* 3 Forcing relation
* 4 References

## Terminology

In this article we use the following terminology.

real
an element of [math]\displaystyle{ 2^\omega }[/math]. In other words, a function that maps each integer to either 0 or 1.
string
an element of [math]\displaystyle{ 2^{\lt \omega} }[/math]. In other words, a finite approximation to a real.

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

condition
An element in a notion of forcing. We say a condition [math]\displaystyle{ p }[/math] is stronger than a condition [math]\displaystyle{ q }[/math] just when [math]\displaystyle{ q \succ_P p }[/math].

compatible conditions
Given conditions [math]\displaystyle{ p,q }[/math] say that [math]\displaystyle{ p }[/math] and [math]\displaystyle{ q }[/math] are compatible if there is a condition [math]\displaystyle{ r }[/math] such that with respect to [math]\displaystyle{ r }[/math], both [math]\displaystyle{ p }[/math] and [math]\displaystyle{ q }[/math] can be simultaneously satisfied if they are true or allowed to coexist.

[math]\displaystyle{ p\mid q }[/math]

means [math]\displaystyle{ p }[/math] and [math]\displaystyle{ q }[/math] are incompatible.

Filter
A subset [math]\displaystyle{ F }[/math] of a notion of forcing [math]\displaystyle{ P }[/math] is a filter if [math]\displaystyle{ p,q \in F \implies p \nmid q }[/math], and [math]\displaystyle{ 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]\displaystyle{ F }[/math] is an ultrafilter if [math]\displaystyle{ F }[/math] is a filter and there is no filter [math]\displaystyle{ F' }[/math] properly containing [math]\displaystyle{ F }[/math].

Cohen forcing
The notion of forcing [math]\displaystyle{ C }[/math] where conditions are elements of [math]\displaystyle{ 2^{\lt \omega} }[/math] and [math]\displaystyle{ (\tau \succ_C \sigma \iff \sigma \supset \tau }[/math])

Note that for Cohen forcing [math]\displaystyle{ \succ_{C} }[/math] is the reverse of the containment relation. This leads to an unfortunate notational confusion where some computability theorists reverse the direction of the forcing partial order (exchanging [math]\displaystyle{ \succ_P }[/math] with [math]\displaystyle{ \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]\displaystyle{ \sigma }[/math] is stronger than [math]\displaystyle{ \tau }[/math] when [math]\displaystyle{ \sigma }[/math] agrees with everything [math]\displaystyle{ \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]\displaystyle{ \tau \succ_C \sigma }[/math] then [math]\displaystyle{ \sigma }[/math] tells us the value of the real at more places.

In a moment we will define a relation [math]\displaystyle{ \sigma \Vdash_P \psi }[/math] (read [math]\displaystyle{ \sigma }[/math] forces [math]\displaystyle{ \psi }[/math]) that holds between conditions (elements of [math]\displaystyle{ P }[/math]) and sentences, but first we need to explain the language that [math]\displaystyle{ \psi }[/math] is a sentence for. However, forcing is a technique, not a definition, and the language for [math]\displaystyle{ \psi }[/math] will depend on the application one has in mind and the choice of [math]\displaystyle{ 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]\displaystyle{ \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]\displaystyle{ V \Vdash \phi }[/math] is used to express that a particular condition or generic set forces a certain proposition or formula [math]\displaystyle{ \phi }[/math] to be true in the resulting forcing extension. Here's [math]\displaystyle{ V }[/math] represents the original universe of sets (the ground model), [math]\displaystyle{ \Vdash }[/math] denotes the forcing relation, and [math]\displaystyle{ \phi }[/math] is a statement in set theory. When [math]\displaystyle{ V \Vdash \phi }[/math], it means that in a suitable forcing extension, the statement [math]\displaystyle{ \phi }[/math] will be true.

## References

* Fitting, Melvin (1981). Fundamentals of generalized recursion theory. Studies in Logic and the Foundations of Mathematics. 105. Amsterdam, New York, and Oxford: North-Holland Publishing Company. pp. 1078–1079. doi:10.2307/2273928.
* Odifreddi, Piergiorgio (1999). Classical recursion theory. Vol. II. Studies in Logic and the Foundations of Mathematics. 143. Amsterdam: North-Holland Publishing Company. ISBN 978-0-444-50205-6.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Forcing (computability). Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Forcing_(computability)&oldid=3382043"