nLab
forcing

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 RR and we want to know what RR would be like if it had a nilsquare element, i.e. an xx such that x 2=0x^2=0, although we don’t know whether RR actually has any nilsquare elements. There are several things we could do.

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

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

  3. We could construct the polynomial ring R[x]R[x] and quotient by the ideal (x 2)(x^2), resulting in the universal ring R[x]/(x 2)R[x]/(x^2) containing RR 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 VV of ZF set theory (for instance), and we want to know what VV would be like if it contained a set GG satisfying some particular properties. We can likewise take three approaches.

  1. We can assume that VV sits inside some larger model of ZF, in such a way that there is a set GG outside of VV and the “model generated by VV and GG” called V[G]V[G] satisfies the desired properties. The GG is called a generic set for the desired “notion of forcing.” There is an extra wrinkle in this approach in that such a GG will not generally exist unless we assume that VV 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 VV, 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 GG 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 VV, 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 VV. The topos of sheaves is moreover universal over VV such that it contains an object GG satisfying the desired properties in its internal logic—in other words, it is a classifying topos of the theory of such a GG. 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

Revised on January 14, 2013 20:43:14 by Urs Schreiber (203.116.137.162)