Forcing (computability): Difference between revisions

Revision as of 14:26, 20 August 2023

Latest revision as of 03:06, 4 June 2025

(5 intermediate revisions by 2 users not shown)

Line 1:

{{Expert needed|mathematics |ex2= logic |reason= Article incomplete |date = April 2021}}

{{Missing information|article|the forcing relation <math>\Vdash</math>|date=April 2021}}

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

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

==Terminology==

Line 17 ⟶ 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 37 ⟶ 35:

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

Line 48 ⟶ 52:

|___location=Amsterdam, New York, and Oxford

|series=Studies in Logic and the Foundations of Mathematics

|pages=1078–1079

|pp=1078-1079

|doi=10.2307/2273928

|volume=105

|jstor=2273928

|s2cid=118376273

}}

*{{Cite book