nLab
forcing

Idea

In set theory, forcing is a way of “adjoining indeterminate objects” to a model in order to make certain axioms true or false in a resulting new model. The language of forcing is generally used in material set theory, but it is more or less equivalent to the construction of categories of sheaves in topos theory and structural set theory.

An analogy to polynomial rings

There are three ways in which to describe the construction of forcing, which can be explained by analogy to a situation in algebra. Suppose that we have a ring $R$ and we want to know what $R$ would be like if it had a nilsquare element, i.e. an $x$ such that $x^2=0$, although we don’t know whether $R$ actually has any nilsquare elements. There are several things we could do.

1. We could consider some larger ring $S$ which contains $R$ as a subring, and also contains some nilsquare element $x$, and then study the subring of $S$ generated by $R$ and $x$, using only our knowledge that it contains $R$ and $x$ and that $x$ is nilsquare.

2. We could work formally in the theory of $R$ with an extra variable $x$ and the axiom that $x^2=0$, avoiding consideration of any new rings at all.

3. We could construct the polynomial ring $R[x]$ and quotient by the ideal $(x^2)$, resulting in the universal ring $R[x]/(x^2)$ containing $R$ and also a nilsquare element.

Obviously these are more or less equivalent ways of doing the same thing. Arguably, most modern mathematicians would find the third the most natural. It is certainly the most category-theoretic and the most in line with the nPOV.

Now suppose instead that we have a model $V$ of ZF set theory (for instance), and we want to know what $V$ would be like if it contained a set $G$ satisfying some particular properties. We can likewise take three approaches.

1. We can assume that $V$ sits inside some larger model of ZF, in such a way that there is a set $G$ outside of $V$ and the “model generated by $V$ and $G$” called $V[G]$ satisfies the desired properties. The $G$ is called a generic set for the desired “notion of forcing.” There is an extra wrinkle in this approach in that such a $G$ will not generally exist unless we assume that $V$ is countable. But for purposes of independence proofs in classical mathematics, this is no problem, since the downward Löwenheim-Skolem theorem? guarantees that if ZF is consistent, then it has a countable model.

2. We can define a new notion of “truth” for statements about $V$, which is not the same as the old one, and which will usually take values not in ordinary truth values but in some more complicated Boolean algebra (or Heyting algebra), in such a way so that the statement “there exists a $G$ with the desired properties” is “true.” This is called forcing semantics.

3. We can construct a new model of set theory out of whole cloth from $V$, rather than trying to find it as a submodel of some assumed larger model. In material set theory, this construction is usually called a Boolean valued model (or a Heyting valued model if it is intuitionistic). In structural set theory, this construction is simply that of the topos of sheaves on a suitable site, in the model $V$. The topos of sheaves is moreover universal over $V$ such that it contains an object $G$ satisfying the desired properties in its internal logic—in other words, it is a classifying topos of the theory of such a $G$. See at References – In terms of classifying toposes for more.

Although by analogy, it would seem that a modern perspective should prefer the third approach, most material set theorists still seem to prefer one of the first two.

Before Cohen? showed how forcing could give rise to models of ZF(C), Fraenkel introduced the method of permutation model?s (later refined by Mostowski and Specker), which gave models of ZFA, a version of ZF with atoms. See for example the basic Fraenkel model.

References

General

• P. J. Cohen, Set theory and the continuum hypothesis, Benjamin, New York 1966

• G. E. Reyes, Typical and generic in a Baire space for relations, thesis 1967

• Abraham Robinson, Infinite forcing in model theory, in Proc. 2nd Scand. Logic Synp. pp. 317-340, ed. J. E. Fenstad

• Jon Barwise ed. Handbook of mathematical logic, 1977, in chapters by Macintyre, Burgess and Keisler

• J. R. Schoenfield, Unramified forcing, pp. 383–395 in: Axiomatic set theory, vol. 1, ed. D. S. Scott, Proc. Symp. Pure Math. 13 (1971)

• math overflow, what is the generic poset used in forcing really?, web

In terms of sheaves and classifying toposes

Reviews of the interpretation of forcing as the passge to classifying toposes include

• Andreas Blass, Andrej Skedrov, Classifying topoi and finite forcing (pdf)

• Andrej Skedrov, Forcing and classifying topoi