Forcing (mathematics)

In the mathematical discipline of set theory, forcing is a technique for proving consistency and independence results. Intuitively, forcing can be thought of as a technique to expand the set theoretical universe to a larger universe by introducing a new "generic" object.
Forcing 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. It 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 computability theory. Descriptive set theory uses the notions of forcing from both computability 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

Forcing is usually used to construct an expanded universe that satisfies some desired property. For example, the expanded universe might contain many new real numbers, identified with subsets of the set of natural numbers, that were not there in the old universe, and thereby violate the continuum hypothesis.
In order to intuitively justify such an expansion, it is best to think of the "old universe" as a model of the set theory, which is itself a set in the "real universe". By the Löwenheim–Skolem theorem, can be chosen to be a "bare bones" model that is externally countable, which guarantees that there will be many subsets of that are not in. Specifically, there is an ordinal that "plays the role of the cardinal " in, but is actually countable in. Working in, it should be easy to find one distinct subset of per each element of.
However, in some sense, it may be desirable to "construct the expanded model within ". This would help ensure that "resembles" in certain aspects, such as being the same as , and allow fine control over the properties of. More precisely, every member of should be given a name in. The name can be thought as an expression in terms of, just like in a simple field extension every element of can be expressed in terms of. A major component of forcing is manipulating those names within, so sometimes it may help to directly think of as "the universe", knowing that the theory of forcing guarantees that will correspond to an actual model.
A subtle point of forcing is that, if is taken to be an arbitrary "missing subset" of some set in, then the constructed "within " may not even be a model. This is because may encode "special" information about that is invisible within , and thus prove the existence of sets that are "too complex for to describe".
Forcing avoids such problems by requiring the newly introduced set to be a generic set relative to. Some statements are "forced" to hold for any generic : For example, a generic is "forced" to be infinite. Furthermore, any property of a generic set is "forced" to hold under some forcing condition. The concept of "forcing" can be defined within, and it gives enough reasoning power to prove that is indeed a model that satisfies the desired properties.
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.

The role of the model

In order for the above approach to work smoothly, must in fact be a standard transitive model in, so that membership and other elementary notions can be handled intuitively in both and. A standard transitive model can be obtained from any standard model through the Mostowski collapse lemma, but the existence of any standard model of is in itself a stronger assumption than the consistency of.
To get around this issue, a standard technique is to let be a standard transitive model of an arbitrary finite subset of , the existence of which is guaranteed by the reflection principle. As the goal of a forcing argument is to prove consistency results, this is enough since any inconsistency in a theory must manifest with a derivation of a finite length, and thus involve only a finite number of axioms.

Forcing conditions and forcing posets

Each forcing condition can be regarded as a finite piece of information regarding the object adjoined to the model. There are many different ways of providing information about an object, which give rise to different forcing notions. A general approach to formalizing forcing notions is to regard forcing conditions as abstract objects with a poset structure.
A forcing poset is an ordered triple,, where is a preorder on, and is the largest element. Members of are the forcing conditions. The order relation means " is stronger than ". Furthermore, the preorder must satisfy the splitting condition:

For each, there are such that, with no such that.

In other words, it must be possible to strengthen any forcing condition in at least two incompatible directions. Intuitively, this is because is only a finite piece of information, whereas an infinite piece of information is needed to determine.
There are various conventions in use. Some authors require 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.

Examples

Let be any infinite set, and let the generic object in question be a new subset. In Cohen's original formulation of forcing, each forcing condition is a finite set of sentences, either of the form or, that are self-consistent. This forcing notion is usually called Cohen forcing.
The forcing poset for Cohen forcing can be formally written as, the finite partial functions from to under reverse inclusion. Cohen forcing satisfies the splitting condition because given any condition, one can always find an element not mentioned in, and add either the sentence or to to get two new forcing conditions, incompatible with each other.
Another instructive example of a forcing poset is, where and is the collection of Borel subsets of having non-zero Lebesgue measure. The generic object associated with this forcing poset is a random real number. It can be shown that falls in every Borel subset of with measure 1, provided that the Borel subset is "described" in the original unexpanded universe. Each forcing condition can be regarded as a random event with probability equal to its measure. Due to the ready intuition this example can provide, probabilistic language is sometimes used with other divergent forcing posets.

Generic filters

Even though each individual forcing condition cannot fully determine the generic object, the set of all true forcing conditions does determine. In fact, without loss of generality, is commonly considered to be the generic object adjoined to, so the expanded model is called. It is usually easy enough to show that the originally desired object is indeed in the model.
Under this convention, the concept of "generic object" can be described in a general way. Specifically, the set should be a generic filter on relative to. The "filter" condition means that it makes sense that is a set of all true forcing conditions:

if, then
if, then there exists an such that

For to be "generic relative to " means:

If is a "dense" subset of , then.

Given that is a countable model, the existence of a generic filter follows from the Rasiowa–Sikorski lemma. In fact, slightly more is true: Given a condition, one can find a generic filter such that. Due to the splitting condition on, if is a filter, then is dense. If, then because is a model of. For this reason, a generic filter is never in.

P-names and interpretations

Associated with a forcing poset is the class of -names. A -name is a set of the form
Given any filter on, the interpretation or valuation map from -names is given by
The -names are, in fact, an expansion of the universe. Given, one defines to be the -name
Since, it follows that. In a sense, is a "name for " that does not depend on the specific choice of.
This also allows defining a "name for " without explicitly referring to :
so that.

Rigorous definitions

The concepts of -names, interpretations, and may be defined by transfinite recursion. With the empty set, the successor ordinal to ordinal, the power-set operator, and a limit ordinal, define the following hierarchy:
Then the class of -names is defined as
The interpretation map and the map can similarly be defined with a hierarchical construction.

Forcing

Given a generic filter, one proceeds as follows. The subclass of -names in is denoted. Let
To reduce the study of the set theory of to that of, one works with the "forcing language", which is built up like ordinary first-order logic, with membership as the binary relation and all the -names as constants.
Define , where is a condition, is a formula in the forcing language, and the 's are -names, to mean that if is a generic filter containing, then. The special case is often written as "" or simply "". Such statements are true in, no matter what is.
What is important is that this external definition of the forcing relation is equivalent to an internal definition within, defined by transfinite induction over the -names on instances of and, and then by ordinary induction over the complexity of formulae. This has the effect that all the properties of are really properties of, and the verification of in becomes straightforward. This is usually summarized as the following three key properties:

Truth: if and only if it is forced by, that is, for some condition, we have.
Definability: The statement "" is definable in.
Coherence:.