Forcing (computability): Difference between revisions

Revision as of 08:08, 9 July 2012

Revision as of 17:39, 14 August 2015

Line 8:

;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>conditions: Given conditions <math>p,q</math> say that <math>p</math> and <math>q</math> are incompatiblecompatible if there is noa condition <math>r</math> with <math> p \succ_P r</math> and <math>q \succ_P r</math>.

;incompatible conditions (noted <math>p\mid q</math>): <math>p</math> is compatible with <math>q</math> if they are not incompatible. <!-- Sometimes we will use '''consistent''' as a synonym for compatible. -->

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

;Ultrafilter : A maximal filter, i.e., <math>F</math> is an ultrafilter if <math>F</math> is a filter and there is no filter <math>F'</math> properly containing <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 recursion 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.