View source for Forcing (mathematics)

{{for|the use of forcing in [[recursion theory]]|Forcing (recursion theory)}}
{{TOC right}}
In the mathematical discipline of [[set theory]], '''forcing''' is a technique for proving [[consistency]] and [[independence (mathematical logic)|independence]] results. It was first used by [[Paul Cohen (mathematician)|Paul Cohen]] in 1963, to prove the independence of the [[axiom of choice]] and the [[continuum hypothesis]] from [[Zermelo–Fraenkel set theory]].

Forcing has been considerably reworked and simplified in the following years, and has since served as a powerful technique, both in set theory and in areas of [[mathematical logic]] such as [[recursion theory]]. [[Descriptive set theory]] uses the notions of forcing from both recursion theory and set theory. Forcing has also been used in [[model theory]], but it is common in model theory to define [[generic filter|genericity]] directly without mention of forcing.

== Intuition ==

Intuitively, forcing consists of expanding the set theoretical [[universe (mathematics)|universe]] <math> V </math> to a larger universe <math> V^{*} </math>. In this bigger universe, for example, one might have many new [[subset]]s of {{nobreak|[[Aleph number#Aleph-naught|<math> \omega </math>]] <math> = \{ 0,1,2,\ldots \} </math>}} that were not there in the old universe, and thereby violate the [[continuum hypothesis]].

While impossible when dealing with finite sets, this is just another version of [[Cantor's paradox]] about infinity. In principle, one could consider:

:<math> V^{*} = V \times \{ 0,1 \}, </math>

identify <math> x \in V </math> with <math> (x,0) </math>, and then introduce an expanded membership relation involving "new" sets of the form <math> (x,1) </math>. Forcing is a more elaborate version of this idea, reducing the expansion to the existence of one new set, and allowing for fine control over the properties of the expanded universe.

Cohen's original technique, now called [[ramified forcing]], is slightly different from the '''unramified forcing''' expounded here. Forcing is also equivalent to the method of [[Boolean-valued model]]s, which some feel is conceptually more natural and intuitive, but usually much more difficult to apply.

== Forcing posets ==

A '''forcing poset''' is an ordered triple, <math> (\mathbb{P},\leq,\mathbf{1}) </math>, where <math> \leq </math> is a [[preorder]] on <math> \mathbb{P} </math> that is '''atomless''', meaning that it satisfies the following condition:

*For each <math> p \in \mathbb{P} </math>, there are <math> q,r \in \mathbb{P} </math> such that <math> q,r \leq p </math>, with no <math> s \in \mathbb{P} </math> such that <math> s \leq q,r </math>. The largest element of <math> \mathbb{P} </math> is <math> \mathbf{1} </math>, that is, <math> p \leq \mathbf{1} </math> for all <math> p \in \mathbb{P} </math>. 
Members of <math> \mathbb{P} </math> are called '''forcing conditions''' or just '''conditions'''. One reads <math> p \leq q </math> as "<math> p </math> is '''stronger''' than <math> q </math>". Intuitively, the "smaller" condition provides "more" information, just as the smaller interval <math> [3.1415926,3.1415927] </math> provides more information about the number [[Pi|<math> \pi </math>]] than the interval <math> [3.1,3.2] </math> does.

There are various conventions in use. Some authors require <math> \leq </math> to also be [[antisymmetric relation|antisymmetric]], so that the relation is a [[partial order]]. Some use the term [[partial order]] anyway, conflicting with standard terminology, while some use the term [[preorder]]. The largest element can be dispensed with. The reverse ordering is also used, most notably by [[Saharon Shelah]] and his co-authors.

=== P-names ===

Associated with a forcing poset <math> \mathbb{P} </math> is the class <math> V^{(\mathbb{P})} </math> of <math> \mathbb{P} </math>-'''names'''. A <math> \mathbb{P} </math>-name is a set <math> A </math> of the form

:<math> A \subseteq \{ (u,p) \mid u ~ \text{is a} ~ \mathbb{P} \text{-name and} ~ p \in \mathbb{P} \}. </math>

This is actually a definition by transfinite recursion. More precisely, one first uses [[transfinite recursion]] to define the following hierarchy:

: <math> \begin{align}
\operatorname{Name}(\varnothing) & = \varnothing; \\
\operatorname{Name}(\alpha + 1)  & = \mathcal{P}(\operatorname{Name}(\alpha) \times \mathbb{P}), \text{ where } \mathcal{P} \text{ denotes the power-set operator}; \\
\operatorname{Name}(\lambda)     & = \bigcup \{ \operatorname{Name}(\alpha) \mid \alpha < \lambda \}, \text{ if } \lambda \text{ is a limit ordinal}.
\end{align} </math>

Then the class of <math> \mathbb{P} </math>-names is defined as

:<math> V^{(\mathbb{P})} = \bigcup \{ \operatorname{Name}(\alpha) ~|~ \alpha ~ \text{is an ordinal} \}. </math>

The <math> \mathbb{P} </math>-names are, in fact, an expansion of the [[von Neumann universe|universe]]. Given <math> x \in V </math>, one defines <math> \check{x} </math> to be the <math> \mathbb{P} </math>-name

:<math> \check{x} = \{ (\check{y},\mathbf{1}) \mid y \in x \}. </math>

Again, this is really a definition by transfinite recursion.

=== Interpretation ===

Given any subset <math> G </math> of <math> \mathbb{P} </math>, one next defines the '''interpretation''' or '''valuation''' map from <math> \mathbb{P} </math>-names by

:<math> \operatorname{val}(u,G) = \{ \operatorname{val}(v,G) \mid \exists p \in G: ~ (v,p) \in u \}. </math>

This is again a definition by transfinite recursion. Note that if <math> \mathbf{1} \in G </math>, then <math> \operatorname{val}(\check{x},G) = x </math>. One then defines

:<math> \underline{G} = \{ (\check{p},p) \mid p \in G \} </math>

so that <math> \operatorname{val}(\underline{G},G) = \{\operatorname{val}(\check p, G) \mid p \in G\} = G </math>.

=== Example ===

A good example of a forcing poset is <math> (\operatorname{Bor}(I),\subseteq,I) </math>, where <math> I = [0,1] </math> and <math> \operatorname{Bor}(I) </math> is the collection of [[Borel subset]]s of <math> I </math> having non-zero [[Lebesgue measure]]. In this case, one can talk about the conditions as being probabilities, and a <math> \operatorname{Bor}(I) </math>-name assigns membership in a probabilistic sense. Due to the ready intuition this example can provide, probabilistic language is sometimes used with other divergent forcing posets.

== Countable transitive models and generic filters ==

The key step in forcing is, given a <math> \mathsf{ZFC} </math> universe <math> V </math>, to find an appropriate object <math> G </math> not in <math> V </math>. The resulting class of all interpretations of <math> \mathbb{P} </math>-names will be a model of <math> \mathsf{ZFC} </math> that properly extends the original <math> V </math> (since <math> G \notin V </math>).

Instead of working with <math> V </math>, it is useful to consider a '''countable transitive model''' <math> M </math> with <math> (\mathbb{P},\leq,\mathbf{1}) \in M </math>. "Model" refers to a model of set theory, either of all of <math> \mathsf{ZFC} </math>, or a model of a large but finite subset of <math> \mathsf{ZFC} </math>, or some variant thereof. "Transitivity" means that if <math> x \in y \in M </math>, then <math> x \in M </math>. The [[Mostowski collapse lemma]] states that this can be assumed if the membership relation is [[well-founded]]. The effect of transitivity is that membership and other elementary notions can be handled intuitively. Countability of the model relies on the [[Löwenheim–Skolem theorem]].

As <math> M </math> is a set, there are sets not in <math> M </math> – this follows from [[Russell's paradox]]. The appropriate set <math> G </math> to pick and adjoin to <math> M </math> is a '''generic filter''' on <math> \mathbb{P} </math>. The "filter" condition means that:

* <math> G \subseteq \mathbb{P}; </math>
* <math> \mathbf{1} \in G; </math>
* if <math> p \geq q \in G </math>, then <math> p \in G; </math>
* if <math> p,q \in G </math>, then there exists an <math> r \in G </math> such that <math> r \leq p,q. </math>

For <math> G </math> to be "generic" means:

* If <math> D \in M </math> is a "dense" subset of <math> \mathbb{P} </math> (that is, for each <math> p \in \mathbb{P} </math>, there exists a <math> q \in D </math> such that <math> q \leq p </math>), then <math> G \cap D \neq \varnothing </math>.

The existence of a generic filter <math> G </math> follows from the [[Rasiowa–Sikorski lemma]]. In fact, slightly more is true: Given a condition <math> p \in \mathbb{P} </math>, one can find a generic filter <math> G </math> such that <math> p \in G </math>. Due to the splitting condition on <math>\mathbb{P}</math> (termed being 'atomless' above), if <math> G </math> is a filter, then <math> \mathbb{P} \setminus G </math> is dense. If <math> G \in M </math>, then <math> \mathbb{P} \setminus G \in M </math> because <math> M </math> is a model of <math> \mathsf{ZFC} </math>. For this reason, a generic filter is never in <math> M </math>.

== Forcing ==

Given a generic filter <math> G \subseteq \mathbb{P}</math>, one proceeds as follows. The subclass of <math> \mathbb{P} </math>-names in <math> M </math> is denoted <math> M^{(\mathbb{P})} </math>. Let 

:<math> M[G] = \left\{ \operatorname{val}(u,G) ~ \Big| ~ u \in M^{(\mathbb{P})} \right\}.</math>

To reduce the study of the set theory of <math> M[G] </math> to that of <math> M </math>, one works with the "forcing language", which is built up like ordinary [[first-order logic]], with membership as the binary relation and all the <math> \mathbb{P} </math>-names as constants.

Define <math> p \Vdash_{M,\mathbb{P}} \varphi(u_{1},\ldots,u_{n}) </math> (to be read as "<math>p</math> forces <math> \varphi </math> in the model <math> M </math> with poset <math> \mathbb{P} </math>"), where <math> p </math> is a condition, <math> \varphi </math> is a formula in the forcing language, and the <math> u_{i} </math>'s are <math> \mathbb{P} </math>-names, to mean that if <math> G </math> is a generic filter containing <math> p </math>, then <math> M[G] \models \varphi(\operatorname{val}(u_{1},G),\ldots,\operatorname{val}(u_{n},G)) </math>. The special case <math> \mathbf{1} \Vdash_{M,\mathbb{P}} \varphi </math> is often written as "<math> \mathbb{P} \Vdash_{M,\mathbb{P}} \varphi </math>" or simply "<math> \Vdash_{M,\mathbb{P}} \varphi </math>". Such statements are true in <math> M[G] </math>, no matter what <math> G </math> is.

What is important is that this '''external''' definition of the forcing relation <math> p \Vdash_{M,\mathbb{P}} \varphi </math> is equivalent to an '''internal''' definition within <math> M </math>, defined by transfinite induction over the <math> \mathbb{P} </math>-names on instances of <math> u \in v </math> and <math> u = v </math>, and then by ordinary induction over the complexity of formulae. This has the effect that all the properties of <math> M[G] </math> are really properties of <math> M </math>, and the verification of <math> \mathsf{ZFC} </math> in <math> M[G] </math> becomes straightforward. This is usually summarized as the following three key properties:

*'''Truth''': <math> M[G] \models \varphi(\operatorname{val}(u_{1},G),\ldots,\operatorname{val}(u_{n},G)) </math> [[if and only if]] it is forced by <math> G </math>, that is, for some condition <math> p \in G </math>, we have <math> p \Vdash_{M,\mathbb{P}} \varphi(u_{1},\ldots,u_{n}) </math>.
*'''Definability''': The statement "<math> p \Vdash_{M,\mathbb{P}} \varphi(u_{1},\ldots,u_{n}) </math>" is definable in <math> M </math>.
*'''Coherence''': <math> p \Vdash_{M,\mathbb{P}} \varphi(u_{1},\ldots,u_{n}) \land q \leq p \implies q \Vdash_{M,\mathbb{P}} \varphi(u_{1},\ldots,u_{n}) </math>.

We define the forcing relation <math> \Vdash_{M,\mathbb{P}} </math> in <math> M </math> by induction on the complexity of formulas, in which we first define the relation for atomic formulas by <math> \in </math>-induction and then define it for arbitrary formulas by induction on their complexity.

We first define the forcing relation on atomic formulas, doing so for both types of formulas, <math>x\in y</math> and <math>x=y</math>, simultaneously. This means that we define one relation <math>R(p,a,b,t,\mathbb{P})</math> where <math>t</math> denotes type of formula as follows:

1. <math>R(p,a,b,0,\mathbb{P})</math> means <math>p\Vdash_{\mathbb{P}}a\in b</math>.

2. <math>R(p,a,b,1,\mathbb{P})</math> means <math>p\Vdash_{\mathbb{P}}a=b</math>.

3. <math>R(p,a,b,2,\mathbb{P})</math> means <math>p\Vdash_{\mathbb{P}}a\subseteq b</math>.

Here <math>p</math> is a condition and <math>a</math> and <math>b</math> are <math>\mathbb{P}</math>-names. Let <math>R(p,a,b,t,\mathbb{P})</math> be a formula defined by <math>\in</math>-induction:

R1. <math>R(p,a,b,0,\mathbb{P})</math> if and only if <math>(\forall q\leq p)(\exists r\leq q)(\exists(s,c)\in b)(r\leq s\,\land\,R(r,a,c,1,\mathbb{P}))</math>.

R2. <math>R(p,a,b,1,\mathbb{P})</math> if and only if <math>R(r,a,b,2,\mathbb{P})\,\land\,R(r,b,a,2,\mathbb{P})</math>.

R3. <math>R(p,a,b,2,\mathbb{P})</math> if and only if <math>(\forall(s,c)\in a)(\forall q\leq p)(\exists r\leq q)(r\leq s\,\Rightarrow\,R(r,c,b,0,\mathbb{P}))</math>.

More formally, we use following binary relation <math>\mathbb{P}</math>-names: Let <math>S(a,b)</math> holds for names <math>a</math> and <math>b</math> if and only if <math>(p,a)\in b</math> for at least one condition <math>p</math>. This relation is well-founded, which means that for any name <math>a</math> the class of all names <math>b</math>, such that <math>S(a,b)</math> holds, is a set and there is no function <math>f:\omega\longrightarrow Names</math> such that <math>(\forall n\in\omega)S(f(n+1),f(n))</math>.

In general a well-founded relation is not a preorder, because it might not be transitive. But, if we consider it as an "ordering", it is a relation without infinite decreasing sequences and where for any element the class of elements below it is a set.

It is easy to close any binary relation for transitivity. For names <math>a</math> and <math>b</math>, <math>a<b</math> holds if there is at least one finite sequence
<math>c_0,\dots,c_n</math> (as a map with domain <math>\{0,\dots,n\}</math>) for some <math>n>0</math> such that <math>c_0=a</math>, <math>c_n=b</math> and for any <math>i<n</math>, <math>S(c_{i-1},c_i)</math> holds. Such an ordering is well-founded too.

We define the following well defined ordering on pairs of names: <math>T((a,b),(c,d))</math> if one of the following holds:

1. <math>\max\{a,b\}<\max\{c,d\}</math>,

2. <math>\max\{a,b\}=\max\{c,d\}</math> and <math>\min\{a,b\}<\min\{c,d\}</math>,

3. <math>\max\{a,b\}=\max\{c,d\}</math> and <math>\min\{a,b\}=\min\{c,d\}</math> and <math>a<c</math>.

The relation <math>R(p,a,b,t,\mathbb{P})</math> is defined by recursion on pairs <math>(a,b)</math> of names. For any pair it is defined by the same relation on "simpler" pairs. Actually, by the recursion theorem there is a formula <math>R(p,a,b,t,\mathbb{P})</math> such that R1, R2 and R3 are theorems because its truth value at some point is defined by its truth values in "smaller" points relative to the some well-founded relation used as an "ordering". Now, we are ready to define forcing relation:

1. <math>p\Vdash_{\mathbb P}a\in b</math> means <math>a,b\in Name\,\land\,R(p,a,b,0,\mathbb{P})</math>.

2. <math>p\Vdash_{\mathbb P}a=b</math> means <math>a,b\in Name\,\land\,R(p,a,b,1,\mathbb{P})</math>.

3. <math>p\Vdash_{\mathbb P}\lnot f(a_1,\dots,a_n)</math> means <math>a_1,\dots,a_n\in Name\,\land\,\lnot(\exists q\leq p)q\Vdash_{\mathbb P} f(a_1,\dots,a_n)</math>.

4. <math>p\Vdash_{\mathbb P}(f(a_1,\dots,a_n)\land g(a_1,\dots,a_n))</math> means <math>a_1,\dots,a_n\in Name\,\land\,(p\Vdash_{\mathbb P}f(a_1,\dots,a_n))\land(p\Vdash_{\mathbb P}g(a_1,\dots,a_n))</math>.

5. <math>p\Vdash_{\mathbb{P}}(\forall x)f(a_1,\dots,a_n,x)</math> means <math>a_1,\dots,a_n\in Name\,\land\,a_1,\dots,a_n\in Name\,\land\,(\forall b\in Names)p\Vdash_{\mathbb{P}}f(a_1,\dots,a_n,b)</math>.

Actually, this is a transformation of an arbitrary formula <math>f(x_1,\dots,x_n)</math> to the formula <math>p\Vdash_{\mathbb{P}}f(x_1,\dots,x_n)</math> where <math>p</math> and <math>\mathbb{P}</math> are additional variables. This is the definition of the forcing relation in the universe <math>V</math> of all sets regardless to any countable transitive model. However, there is a relation between this "syntactic" formulation of forcing and the "semantic" formulation of forcing over some countable transitive model <math>M</math>.

1. For any formula <math>f(x_1,\dots,x_n)</math> there is a theorem <math>T</math> of the theory <math>ZFC</math> (for example conjunction of finite number of axioms) such that for any countable transitive model <math>M</math> such that <math>M\models T</math> and any atomless partial order <math>\mathbb{P}\in M</math> and any <math>\mathbb{P}</math>-generic filter <math>G</math> over <math>M</math>

:<math>(\forall a_1,\ldots,a_n\in M^{\mathbb{P}})(\forall p\in\mathbb{P})(p\Vdash_{M,\mathbb{P}} f(a_1,\dots,a_n) \,\Leftrightarrow \, M\models p\Vdash_{\mathbb{P}}f(a_1,\dots,a_n)).</math>

This is called the property of definability of the forcing relation.

== Consistency ==

The discussion above can be summarized by the fundamental consistency result that, given a forcing poset <math> \mathbb{P} </math>, we may assume the existence of a generic filter <math> G </math>, not belonging to the universe <math> V </math>, such that <math> V[G] </math> is again a set-theoretic universe that models <math> \mathsf{ZFC} </math>. Furthermore, all truths in <math> V[G] </math> may be reduced to truths in <math> V </math> involving the forcing relation.

Both styles, adjoining <math> G </math> to either a countable transitive model <math> M </math> or the whole universe <math> V </math>, are commonly used. Less commonly seen is the approach using the "internal" definition of forcing, in which no mention of set or class models is made. This was Cohen's original method, and in one elaboration, it becomes the method of Boolean-valued analysis.

== {{vanchor|Cohen forcing}} ==

The simplest nontrivial forcing poset is <math> (\operatorname{Fin}(\omega,2),\supseteq,0) </math>, the finite partial functions from <math> \omega </math> to <math> 2 ~ \stackrel{\text{df}}{=} ~ \{ 0,1 \} </math> under ''reverse'' inclusion. That is, a condition <math> p </math> is essentially two disjoint finite subsets <math> {p^{-1}}[1] </math> and <math> {p^{-1}}[0] </math> of <math> \omega </math>, to be thought of as the "yes" and "no" parts of {{nowrap|<math> p </math>,}} with no information provided on values outside the domain of <math> p </math>. "<math> q </math> is stronger than <math> p </math>" means that <math> q \supseteq p </math>, in other words, the "yes" and "no" parts of <math> q </math> are supersets of the "yes" and "no" parts of <math> p </math>, and in that sense, provide more information.

Let <math> G </math> be a generic filter for this poset. If <math> p </math> and <math> q </math> are both in <math> G </math>, then <math> p \cup q </math> is a condition because <math> G </math> is a filter. This means that <math> g = \bigcup G </math> is a well-defined partial function from <math> \omega </math> to <math> 2 </math> because any two conditions in <math> G </math> agree on their common domain.

In fact, <math> g </math> is a total function. Given <math> n \in \omega </math>, let <math> D_{n} = \{ p \mid p(n) ~ \text{is defined} \} </math>. Then <math> D_{n} </math> is dense. (Given any <math> p </math>, if <math> n </math> is not in <math> p </math>'s domain, adjoin a value for <math> n </math>—the result is in <math> D_{n} </math>.) A condition <math> p \in G \cap D_{n} </math> has <math> n </math> in its domain, and since <math> p \subseteq g </math>, we find that <math> g(n) </math> is defined.

Let <math> X = {g^{-1}}[1] </math>, the set of all "yes" members of the generic conditions. It is possible to give a name for <math> X </math> directly. Let 

:<math> \underline{X} = \left \{ \left (\check{n},p \right ) \mid p(n) = 1 \right \}.</math>

Then <math>\operatorname{val}(\underline{X},G) = X.</math> Now suppose that <math> A \subseteq \omega </math> in <math> V </math>. We claim that <math> X \neq A </math>. Let 

:<math> D_{A} = \{ p \mid (\exists n)(n \in \operatorname{Dom}(p) \land (p(n) = 1 \iff n \notin A)) \}.</math>

Then <math>D_A</math> is dense. (Given any <math> p </math>, if <math> n </math> is not in its domain, adjoin a value for <math> n </math> contrary to the status of "<math> n \in A </math>".) Then any <math> p \in G \cap D_A</math> witnesses <math> X \neq A </math>. To summarize, <math> X </math> is a "new" subset of <math> \omega </math>, necessarily infinite.

Replacing <math> \omega </math> with <math> \omega \times \omega_{2} </math>, that is, consider instead finite partial functions whose inputs are of the form <math> (n,\alpha) </math>, with <math> n < \omega </math> and <math> \alpha < \omega_{2} </math>, and whose outputs are <math> 0 </math> or <math> 1 </math>, one gets <math> \omega_{2} </math> new subsets of <math> \omega </math>. They are all distinct, by a density argument: Given <math> \alpha < \beta < \omega_{2} </math>, let 

:<math> D_{\alpha,\beta} = \{ p \mid (\exists n)(p(n,\alpha) \neq p(n,\beta)) \},</math> 

then each <math> D_{\alpha,\beta} </math> is dense, and a generic condition in it proves that the αth new set disagrees somewhere with the <math> \beta </math>th new set.

This is not yet the falsification of the continuum hypothesis. One must prove that no new maps have been introduced which map <math> \omega </math> onto <math> \omega_{1} </math>, or <math> \omega_{1} </math> onto <math> \omega_{2} </math>. For example, if one considers instead <math> \operatorname{Fin}(\omega,\omega_{1}) </math>, finite partial functions from <math> \omega </math> to <math> \omega_{1} </math>, the [[first uncountable ordinal]], one gets in <math> V[G] </math> a bijection from <math> \omega </math> to <math> \omega_{1} </math>. In other words, <math> \omega_{1} </math> has ''collapsed'', and in the forcing extension, is a countable ordinal.

The last step in showing the independence of the continuum hypothesis, then, is to show that Cohen forcing does not collapse cardinals. For this, a sufficient combinatorial property is that all of the [[antichain]]s of the forcing poset are countable.

== The countable chain condition ==

{{main article|Countable chain condition}}
An [[strong antichain|(strong) antichain]] <math> A </math> of <math> \mathbb{P} </math> is a subset such that if <math> p,q \in A </math>, then <math> p </math> and <math> q </math> are '''incompatible''' (written <math> p \perp q </math>), meaning there is no <math> r </math> in <math> \mathbb{P} </math> such that <math> r \leq p </math> and <math> r \leq q </math>.  In the example on Borel sets, incompatibility means that <math> p \cap q </math> has zero measure. In the example on finite partial functions, incompatibility means that <math> p \cup q </math> is not a function, in other words, <math> p </math> and <math> q </math> assign different values to some domain input.

<math> \mathbb{P} </math> satisfies the [[countable chain condition]] (c.c.c.) if and only if every antichain in <math> \mathbb{P} </math> is countable. (The name, which is obviously inappropriate, is a holdover from older terminology. Some mathematicians write "c.a.c." for "countable antichain condition".)

It is easy to see that <math> \operatorname{Bor}(I) </math> satisfies the c.c.c. because the measures add up to at most <math> 1 </math>. Also, <math> \operatorname{Fin}(E,2) </math> satisfies the c.c.c., but the proof is more difficult.

Given an uncountable subfamily <math> W \subseteq \operatorname{Fin}(E,2) </math>, shrink <math> W </math> to an uncountable subfamily <math> W_{0} </math> of sets of size <math> n </math>, for some <math>n < \omega </math>. If <math> p(e_{1}) = b_{1} </math> for uncountably many <math> p \in W_{0} </math>, shrink this to an uncountable subfamily <math> W_{1} </math> and repeat, getting a finite set <math> \{ (e_{1},b_{1}),\ldots,(e_{k},b_{k}) \} </math> and an uncountable family <math> W_{k} </math> of incompatible conditions of size <math> n - k </math> such that every <math> e </math> is in <math> \operatorname{Dom}(p) </math> for at most countable many <math> p \in W_{k} </math>. Now, pick an arbitrary <math> p \in W_{k} </math>, and pick from <math> W_{k} </math> any <math> q </math> that is not one of the countably many members that have a domain member in common with <math> p </math>. Then <math> p \cup \{ (e_{1},b_{1}),\ldots,(e_{k},b_{k}) \} </math> and <math>q \cup \{ (e_{1},b_{1}),\ldots,(e_{k},b_{k}) \} </math> are compatible, so <math> W </math> is not an antichain. In other words, <math> \operatorname{Fin}(E,2) </math>-antichains are countable.

The importance of antichains in forcing is that for most purposes, dense sets and maximal antichains are equivalent. A ''maximal'' antichain <math> A </math> is one that cannot be extended to a larger antichain. This means that every element <math> p \in \mathbb{P} </math> is compatible with some member of <math> A </math>. The existence of a maximal antichain follows from [[Zorn's lemma|Zorn's Lemma]]. Given a maximal antichain <math> A </math>, let 

:<math> D = \left \{ p \in \mathbb{P} \mid (\exists q \in A)(p \leq q) \right \}.</math>

Then <math> D </math> is dense, and <math> G \cap D \neq \varnothing </math> if and only if <math> G \cap A \neq \varnothing </math>. Conversely, given a dense set <math> D </math>, Zorn's Lemma shows that there exists a maximal antichain <math> A \subseteq D </math>, and then <math> G \cap D \neq \varnothing </math> if and only if <math> G \cap A \neq \varnothing </math>.

Assume that <math> \mathbb{P} </math> satisfies the c.c.c. Given <math> x,y \in V </math>, with <math> f: x \to y </math> a function in <math> V[G] </math>, one can approximate <math> f </math> inside <math> V </math> as follows. Let <math> u </math> be a name for <math> f </math> (by the definition of <math> V[G] </math>) and let <math> p </math> be a condition that forces <math> u </math> to be a function from <math> x </math> to <math> y </math>. Define a function <math> F </math>, whose domain is <math> x </math>, by 

:<math> F(a) \stackrel{\text{df}}{=} \left \{ b \left | (\exists q \in \mathbb{P}) \left [(q \leq p) \land \left (q \Vdash ~ u \left (\check{a} \right ) = \check{b} \right ) \right ] \right \}. \right.</math> 

By the definability of forcing, this definition makes sense within <math> V </math>. By the coherence of forcing, a different <math> b </math> come from an incompatible <math> p </math>. By c.c.c., <math> F(a) </math> is countable.

In summary, <math> f </math> is unknown in <math> V </math> as it depends on <math> G </math>, but it is not wildly unknown for a c.c.c.-forcing. One can identify a countable set of guesses for what the value of <math> f </math> is at any input, independent of <math> G </math>.

This has the following very important consequence. If in <math> V[G] </math>, <math> f: \alpha \to \beta </math> is a surjection from one infinite ordinal onto another, then there is a surjection <math> g: \omega \times \alpha \to \beta </math> in <math> V </math>, and consequently, a surjection <math> h: \alpha \to \beta </math> in <math> V </math>. In particular, cardinals cannot collapse. The conclusion is that <math>2^{\aleph_{0}} \geq \aleph_{2} </math> in <math> V[G] </math>.

== {{vanchor|Easton forcing}} ==

The exact value of the continuum in the above Cohen model, and variants like <math> \operatorname{Fin}(\omega \times \kappa,2) </math> for cardinals <math> \kappa </math> in general, was worked out by [[Robert M. Solovay]], who also worked out how to violate <math> \mathsf{GCH} </math> (the [[Continuum hypothesis#The generalized continuum hypothesis|generalized continuum hypothesis]]), for [[regular cardinal]]s only, a finite number of times. For example, in the above Cohen model, if <math> \mathsf{CH} </math> holds in <math> V </math>, then <math> 2^{\aleph_{0}} = \aleph_{2} </math> holds in <math> V[G] </math>.

[[William Bigelow Easton|William B. Easton]] worked out the proper class version of violating the <math> \mathsf{GCH} </math> for regular cardinals, basically showing that the known restrictions, (monotonicity, [[Cantor's theorem|Cantor's Theorem]] and [[König's theorem (set theory)|König's Theorem]]), were the only <math> \mathsf{ZFC} </math>-provable restrictions (see [[Easton's theorem|Easton's Theorem]]).

Easton's work was notable in that it involved forcing with a proper class of conditions. In general, the method of forcing with a proper class of conditions fails to give a model of <math> \mathsf{ZFC} </math>. For example, forcing with <math> \operatorname{Fin}(\omega \times \mathbf{On},2) </math>, where <math> \mathbf{On} </math> is the proper class of all ordinals, makes the continuum a proper class. On the other hand, forcing with <math> \operatorname{Fin}(\omega,\mathbf{On}) </math> introduces a countable enumeration of the ordinals. In both cases, the resulting <math> V[G] </math> is visibly not a model of <math> \mathsf{ZFC} </math>.

At one time, it was thought that more sophisticated forcing would also allow an arbitrary variation in the powers of [[Regular cardinal|singular cardinal]]s. However, this has turned out to be a difficult, subtle and even surprising problem, with several more [[PCF theory|restrictions provable]] in <math> \mathsf{ZFC} </math> and with the forcing models depending on the consistency of various [[large cardinal|large-cardinal]] properties. Many open problems remain.

== Random reals ==

{{main article|Random algebra}}

Random forcing can be defined as forcing over the set <math>P</math> of all compact subsets of <math>[0,1]</math> of positive measure ordered by relation <math>\subseteq</math> (smaller set in context of inclusion is smaller set in ordering and represents condition with more information). There are two types of important dense sets:

1. For any positive integer <math>n</math> the set 

:<math>D_n= \left \{p\in P : \operatorname{diam}(p)<\frac 1n \right \}</math> 

is dense, where <math>\operatorname{diam}(p)</math> is diameter of the set <math>p</math>.

2. For any Borel subset <math>B \subseteq [0,1]</math> of measure 1, the set 

:<math>D_B=\{p\in P : p\subseteq B\}</math> 

is dense.

For any filter <math>G</math> and for any finitely many elements <math>p_1,\ldots,p_n\in G</math> there is <math>q\in G</math> such that holds <math>q\leq p_1,\ldots,p_n</math>. In case of this ordering, this means that any filter is set of compact sets with finite intersection property. For this reason, intersection of all elements of any filter is nonempty. Let <math>G</math> is filter intersecting dense set <math>D_n</math> for any positive integer <math>n</math>, then filter <math>G</math> contains conditions of arbitrary small positive diameter. Therefore, intersection of all conditions from <math>G</math> has diameter 0. Only nonempty sets of diameter 0 are singletons. Finally, there is exactly one real number <math>r</math> such that <math>r\in\bigcap G</math>.

Let <math>B\subseteq[0,1]</math> is any Borel set of measure 1. If <math>G</math> intersects <math>D_B</math>, then <math>r\in B</math>.

However, generic filter over countable transitive model <math>V</math> is not in <math>V</math>. Real <math>r</math> is defined by <math>G</math>. One can also prove that it is not in <math>V</math>. The problem is that if <math>p\in P</math>, then <math>V\models</math>"<math>p</math> is compact", but from the viewpoint of universe <math>p</math> can be non-compact and the intersection of all conditions from generic filter is actually empty. For this reason, we consider set <math>C=\{\bar p : p\in G\}</math> of closures (in topological sense) of conditions from generic filter.{{clarify|date=July 2018}} Due to <math>\bar p\supseteq p</math> and finite intersection property of <math>G</math>, the set <math>C</math> also has finite intersection property. Elements of the set <math>C</math> are bounded closed sets as closures of bounded sets.{{clarify|date=July 2018}} Therefore, <math>C</math>
is set of compacts{{clarify|date=July 2018}} with finite intersection property and for this reason has nonempty intersection. Due to <math>\operatorname{diam}(\bar p) = \operatorname{diam}(p)</math> and model <math>V</math> inherits metric from universe, the set <math>C</math> has elements of arbitrary small diameter. Finally, there is exactly one real that belongs to all members of the set <math>C</math>. The generic filter <math>G</math> can be reconstructed from <math>r</math> as <math>G=\{p\in P : r\in\bar p\}</math>.

If <math>a</math> is name of <math>r</math>,{{clarify|date=July 2018}} and for <math>B\in V</math> holds <math>V\models</math>"<math>B</math> is Borel set of measure 1", then holds 

:<math>V[G]\models \left (p\Vdash_{\mathbb{P}}a\in\check{B} \right )</math> 

for some <math>p\in G</math>. There is name <math>a</math> such that for any generic filter <math>G</math> holds 

:<math>\operatorname{val}(a,G)\in\bigcup_{p\in G}\bar p.</math> 

Then 

:<math>V[G]\models \left (p\Vdash_{\mathbb{P}}a\in\check{B} \right )</math> 

holds for any condition <math>p</math>.

Every Borel set can, non-uniquely, be built up, starting from intervals with rational endpoints and applying the operations of complement and countable unions, a countable number of times. The record of such a construction is called a ''Borel code''. Given a Borel set <math>B</math> in <math>V</math>, one recovers a Borel code, and then applies the same construction sequence in <math>V[G]</math>, getting a Borel set <math>B^*</math>. It can be proven that one gets the same set independent of the construction of <math>B </math>, and that basic properties are preserved. For example, if <math>B \subseteq C</math>, then <math>B^* \subseteq C^*</math>. If <math>B</math> has measure zero, then <math>B^*</math> has measure zero. This mapping <math>B\mapsto B^*</math> is injective.

For any set <math>B\subseteq[0,1]</math> such that <math>B\in V</math> and <math>V\models</math>"<math>B</math> is Borel set of measure 1" holds <math>r\in B^*</math>.

This means that <math>r</math> is "infinite random sequence of 0s and 1s" from the viewpoint of <math>V</math>, which means that it satisfies all statistical tests from the ground model <math>V</math>.

So given <math>r</math>, a random real, one can show that 

:<math> G = \left \{ B ~ (\text{in } V) \mid r \in B^* ~ (\text{in } V[G]) \right \}. </math>

Because of the mutual inter-definability between <math>r</math> and <math> G </math>, one generally writes <math>V[r]</math> for <math>V[G]</math>.

A different interpretation of reals in <math>V[G]</math> was provided by [[Dana Scott]]. Rational numbers in <math> V[G] </math> have names that correspond to countably-many distinct rational values assigned to a maximal antichain of Borel sets – in other words, a certain rational-valued function on <math>I = [0,1] </math>. Real numbers in <math>V[G]</math> then correspond to [[Dedekind cut]]s of such functions, that is, [[measurable function]]s.

== Boolean-valued models ==
{{main article|Boolean-valued model}}

Perhaps more clearly, the method can be explained in terms of Boolean-valued models. In these, any statement is assigned a [[truth value]] from some complete atomless [[Boolean algebra (structure)|Boolean algebra]], rather than just a true/false value. Then an [[ultrafilter]] is picked in this Boolean algebra, which assigns values true/false to statements of our theory. The point is that the resulting theory has a model which contains this ultrafilter, which can be understood as a new model obtained by extending the old one with this ultrafilter. By picking a Boolean-valued model in an appropriate way, we can get a model that has the desired property. In it, only statements which must be true (are "forced" to be true) will be true, in a sense (since it has this extension/minimality property).

== Meta-mathematical explanation ==

In forcing, we usually seek to show that some [[sentence (mathematical logic)|sentence]] is [[Consistency proof|consistent]] with <math> \mathsf{ZFC} </math> (or optionally some extension of <math> \mathsf{ZFC} </math>). One way to interpret the argument is to assume that <math> \mathsf{ZFC} </math> is consistent and then prove that <math> \mathsf{ZFC} </math> combined with the new [[sentence (mathematical logic)|sentence]] is also consistent.

Each "condition" is a finite piece of information – the idea is that only finite pieces are relevant for consistency, since, by the [[compactness theorem]], a theory is satisfiable if and only if every finite subset of its axioms is satisfiable. Then we can pick an infinite set of consistent conditions to extend our model. Therefore, assuming the consistency of <math> \mathsf{ZFC} </math>, we prove the consistency of <math> \mathsf{ZFC} </math> extended by this infinite set.

== Logical explanation ==

By [[Gödel's second incompleteness theorem]], one cannot prove the consistency of any sufficiently strong formal theory, such as <math> \mathsf{ZFC} </math>, using only the axioms of the theory itself, unless the theory is inconsistent. Consequently, mathematicians do not attempt to prove the consistency of <math> \mathsf{ZFC} </math> using only the axioms of <math> \mathsf{ZFC} </math>, or to prove that <math> \mathsf{ZFC} + H </math> is consistent for any hypothesis <math> H </math> using only <math> \mathsf{ZFC} + H </math>. For this reason, the aim of a consistency proof is to prove the consistency of <math> \mathsf{ZFC} + H </math> relative to the consistency of <math> \mathsf{ZFC} </math>. Such problems are known as problems of '''relative consistency''', one of which proves

(*) <math> \mathsf{ZFC} \vdash \operatorname{Con}(\mathsf{ZFC}) \rightarrow \operatorname{Con}(\mathsf{ZFC} + H). </math>

The general schema of relative consistency proofs follows. As any proof is finite, it uses only a finite number of axioms:

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash (\exists T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \land (T \vdash \lnot H)). </math>

For any given proof, <math> \mathsf{ZFC} </math> can verify the validity of this proof. This is provable by induction on the length of the proof.

: <math> \mathsf{ZFC} \vdash (\forall T)((T \vdash \lnot H) \rightarrow (\mathsf{ZFC} \vdash (T \vdash \lnot H))). </math>

Then resolve

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash (\exists T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \land (\mathsf{ZFC} \vdash (T \vdash \lnot H))). </math>

By proving the following

(**) <math> \mathsf{ZFC} \vdash (\forall T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \rightarrow (\mathsf{ZFC} \vdash \operatorname{Con}(T + H))), </math>

it can be concluded that

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash (\exists T)(\operatorname{Fin}(T) \land T \subseteq \mathsf{ZFC} \land (\mathsf{ZFC} \vdash (T \vdash \lnot H)) \land (\mathsf{ZFC} \vdash \operatorname{Con}(T + H))), </math>

which is equivalent to

: <math> \mathsf{ZFC} + \lnot \operatorname{Con}(\mathsf{ZFC} + H) \vdash \lnot \operatorname{Con}(\mathsf{ZFC}), </math>

which gives (*). The core of the relative consistency proof is proving (**). A <math> \mathsf{ZFC} </math> proof of <math> \operatorname{Con}(T + H) </math> can be constructed for any given finite subset <math> T </math> of the <math> \mathsf{ZFC} </math> axioms (by <math> \mathsf{ZFC} </math> instruments of course). (No universal proof of <math> \operatorname{Con}(T + H) </math> of course.)

In <math> \mathsf{ZFC} </math>, it is provable that for any condition <math> p </math>, the set of formulas (evaluated by names) forced by <math> p </math> is deductively closed. Furthermore, for any <math> \mathsf{ZFC} </math> axiom, <math> \mathsf{ZFC} </math> proves that this axiom is forced by <math> \mathbf{1} </math>. Then it suffices to prove that there is at least one condition that forces <math> H </math>.

In the case of Boolean-valued forcing, the procedure is similar: proving that the Boolean value of <math> H </math> is not <math> \mathbf{0} </math>.

Another approach uses the Reflection Theorem. For any given finite set of <math> \mathsf{ZFC} </math> axioms, there is a <math> \mathsf{ZFC} </math> proof that this set of axioms has a countable transitive model. For any given finite set <math> T </math> of <math> \mathsf{ZFC} </math> axioms, there is a finite set <math> T' </math> of <math> \mathsf{ZFC} </math> axioms such that <math> \mathsf{ZFC} </math> proves that if a countable transitive model <math> M </math> satisfies <math> T' </math>, then <math> M[G] </math> satisfies <math> T </math>. By proving that there is finite set <math> T'' </math> of <math> \mathsf{ZFC} </math> axioms such that if a countable transitive model <math> M </math> satisfies <math> T'' </math>, then <math> M[G] </math> satisfies the hypothesis <math> H </math>. Then, for any given finite set <math> T </math> of <math> \mathsf{ZFC} </math> axioms, <math> \mathsf{ZFC} </math> proves <math> \operatorname{Con}(T + H) </math>.

Sometimes in (**), a stronger theory <math> S </math> than <math> \mathsf{ZFC} </math> is used for proving <math> \operatorname{Con}(T + H) </math>. Then we have proof of the consistency of <math> \mathsf{ZFC} + H </math> relative to the consistency of <math> S </math>. Note that <math> \mathsf{ZFC} \vdash \operatorname{Con}(\mathsf{ZFC}) \leftrightarrow \operatorname{Con}(\mathsf{ZFL}) </math>, where <math> \mathsf{ZFL} </math> is <math> \mathsf{ZF} + V = L </math> (the axiom of constructibility).

== See also ==
*[[List of forcing notions]]
*[[Nice name]]

== References ==
* Bell, J. L. (1985). ''Boolean-Valued Models and Independence Proofs in Set Theory'', Oxford. {{ISBN|0-19-853241-5}}
* {{cite book|author = Cohen, P. J.|title = Set theory and the continuum hypothesis|year = 1966|publisher = Addison–Wesley|isbn = 978-0-8053-2327-6}}
* {{springer|id = F/f040770|title = Forcing Method|first = V. N.|last = Grishin}}
* {{cite book|title = Set Theory: An Introduction to Independence Proofs|author = Kunen, K.|publisher = North-Holland|year = 1980|isbn = 978-0-444-85401-8|title-link = Set Theory: An Introduction to Independence Proofs}}

== External links ==
*Nik Weaver's book [http://www.worldscientific.com/worldscibooks/10.1142/8962 Forcing for Mathematicians] was written for mathematicians who want to learn the basic machinery of forcing. No background in logic is assumed, beyond the facility with formal syntax which should be second nature to any well-trained mathematician.
*[[Timothy Chow]]'s article [https://arxiv.org/abs/0712.1320 A Beginner's Guide to Forcing] is a good introduction to the concepts of forcing that avoids a lot of technical detail.  This paper grew out of Chow's newsgroup article [http://alum.mit.edu/www/tchow/mathstuff/forcingdum Forcing for dummies].  In addition to improved exposition, the Beginner's Guide includes a section on Boolean-valued models.
*See also [[Kenny Easwaran]]'s article [https://arxiv.org/abs/0712.2279 A Cheerful Introduction to Forcing and the Continuum Hypothesis], which is also aimed at the beginner but includes more technical details than Chow's article.
*Cohen, P. J. [https://dx.doi.org/10.1073/pnas.50.6.1143 ''The Independence of the Continuum Hypothesis''], Proceedings of the National Academy of Sciences of the United States of America, Vol. 50, No. 6. (Dec. 15, 1963), pp.&nbsp;1143–1148.
*Cohen, P. J. [https://dx.doi.org/10.1073/pnas.51.1.105 ''The Independence of the Continuum Hypothesis, II''], Proceedings of the National Academy of Sciences of the United States of America, Vol. 51, No. 1. (Jan. 15, 1964), pp.&nbsp;105–110.
*Paul Cohen gave a historical lecture [http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.rmjm/1181070010 The Discovery of Forcing] (Rocky Mountain J. Math. Volume 32, Number 4 (2002), 1071–1100) about how he developed his independence proof.  The linked page has a download link for an open access PDF but your browser must send a [[referer]] header from the linked page to retrieve it.
*Akihiro Kanamori: [http://math.bu.edu/people/aki/16.pdf ''Set theory from Cantor to Cohen'']
*{{MathWorld|title = Forcing|id = Forcing}}

{{Set theory}}

[[Category:Forcing (mathematics)| ]]