Forcing (mathematics)

In the mathematical discipline of set theory, forcing is a technique for proving consistency and independence results. It was first used by 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 genericity directly without mention of forcing.

Intuition

Intuitively, forcing consists of expanding the set theoretical universe $V$ to a larger universe $V^$. In this bigger universe, for example, one might have many new real numbers, identified with subsets of the set $\mathbb$ of natural numbers, 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:

:$V^ = V \times \,$

identify $x \in V$ with $(x,0)$, and then introduce an expanded membership relation involving "new" sets of the form $(x,1)$. 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 models, 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, $(\mathbb,\leq,\mathbf)$, where $\leq$ is a preorder on $\mathbb$ that is atomless, meaning that it satisfies the following condition:

*For each $p \in \mathbb$, there are $q,r \in \mathbb$ such that $q,r \leq p$, with no $s \in \mathbb$ such that $s \leq q,r$. The largest element of $\mathbb$ is $\mathbf$, that is, $p \leq \mathbf$ for all $p \in \mathbb$.
Members of $\mathbb$ are called forcing conditions or just conditions. One reads $p \leq q$ as "$p$ is stronger than $q$". Intuitively, the "smaller" condition provides "more" information, just as the smaller interval .1415926,3.1415927 provides more information about the number than the interval .1,3.2 does.

There are various conventions in use. Some authors require $\leq$ to also be 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 $\mathbb$ is the class $V^$ of $\mathbb$-names. A $\mathbb$-name is a set $A$ of the form

:$A \subseteq \.$

This is actually a definition by transfinite recursion. With $\varnothing$ the empty set, $\alpha + 1$ the successor ordinal to ordinal $\alpha$, $\mathcal$ the power-set operator, and $\lambda$ a limit ordinal, define the following hierarchy:

: $\begin \operatorname(\varnothing) & = \varnothing, \\ \operatorname(\alpha + 1) & = \mathcal(\operatorname(\alpha) \times \mathbb), \\ \operatorname(\lambda) & = \bigcup \. \end$

Then the class of $\mathbb$-names is defined as

:$V^ = \bigcup \.$

The $\mathbb$-names are, in fact, an expansion of the universe. Given $x \in V$, one defines $\check$ to be the $\mathbb$-name

:$\check = \.$

Again, this is really a definition by transfinite recursion.

Interpretation

Given any subset $G$ of $\mathbb$, one next defines the interpretation or valuation map from $\mathbb$-names by

:$\operatorname(u,G) = \.$

This is again a definition by transfinite recursion. Note that if $\mathbf \in G$, then $\operatorname(\check,G) = x$. One then defines

:$\underline = \$

so that $\operatorname(\underline,G) = \ = G$.

Example

A good example of a forcing poset is $(\operatorname(I),\subseteq,I)$, where I = ,1 and $\operatorname(I)$ is the collection of Borel subsets of $I$ having non-zero Lebesgue measure. In this case, one can talk about the conditions as being probabilities, and a $\operatorname(I)$-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 $\mathsf$ universe $V$, to find an appropriate object $G$ not in $V$. The resulting class of all interpretations of $\mathbb$-names will be a model of $\mathsf$ that properly extends the original $V$ (since $G \notin V$).

Instead of working with $V$, it is useful to consider a countable transitive model $M$ with $(\mathbb,\leq,\mathbf) \in M$. "Model" refers to a model of set theory, either of all of $\mathsf$, or a model of a large but finite subset of $\mathsf$, or some variant thereof. "Transitivity" means that if $x \in y \in M$, then $x \in M$. 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 $M$ is a set, there are sets not in $M$ – this follows from Russell's paradox. The appropriate set $G$ to pick and adjoin to $M$ is a generic filter on $\mathbb$. The "filter" condition means that:

* $G \subseteq \mathbb;$
* $\mathbf \in G;$
* if $p \geq q \in G$, then $p \in G;$
* if $p,q \in G$, then there exists an $r \in G$ such that $r \leq p,q.$

For $G$ to be "generic" means:

* If $D \in M$ is a "dense" subset of $\mathbb$ (that is, for each $p \in \mathbb$, there exists a $q \in D$ such that $q \leq p$), then $G \cap D \neq \varnothing$.

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

Forcing

Given a generic filter $G \subseteq \mathbb$, one proceeds as follows. The subclass of $\mathbb$-names in $M$ is denoted $M^$. Let

: M = \left\.

To reduce the study of the set theory of M to that of $M$, one works with the "forcing language", which is built up like ordinary first-order logic, with membership as the binary relation and all the $\mathbb$-names as constants.

Define $p \Vdash_ \varphi(u_1,\ldots,u_n)$ (to be read as "$p$ forces $\varphi$ in the model $M$ with poset $\mathbb$"), where $p$ is a condition, $\varphi$ is a formula in the forcing language, and the $u_$'s are $\mathbb$-names, to mean that if $G$ is a generic filter containing $p$, then M \models \varphi(\operatorname(u_1,G),\ldots,\operatorname(u_,G)) . The special case $\mathbf \Vdash_ \varphi$ is often written as "$\mathbb \Vdash_ \varphi$" or simply "$\Vdash_ \varphi$". Such statements are true in M , no matter what $G$ is.

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

*Truth: M \models \varphi(\operatorname(u_1,G),\ldots,\operatorname(u_n,G)) if and only if it is forced by $G$, that is, for some condition $p \in G$, we have $p \Vdash_ \varphi(u_1,\ldots,u_n)$.
*Definability: The statement "$p \Vdash_ \varphi(u_1,\ldots,u_n)$" is definable in $$