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. From the point of view of structural set theory/categorical logic it is more or less equivalent to the construction of categories of sheaves in topos theory and structural set theory: here a classifying topos of a theory is a “category of sets” that is “forced” to contain a generic model of the 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 (Shulman 20), 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 models (later refined by Mostowski and Specker), which gave models of ZFA, a version of ZF with atoms. See for example the basic Fraenkel model.

Related concepts

• Kripke-Joyal semantics

• double negation topology

• homotopy type theory FAQ– What is homotopy type theory? – For set theorists

References

Exposition is in

• Timothy Chow, A beginner’s guide to forcing, Contemp. Math (arXiv:0712.1320)

Another good introduction is in Schoenfield 71

General

• Paul Cohen, Set theory and the continuum hypothesis, Benjamin, New York 1966

• Gonzalo 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) ((pdf))

• S. Shelah, Proper and Improper Forcing , Perspectives in Math. Logic vol. 5 Springer Heidelberg 1998. (toc)

• Paul Cohen, The Discovery of Forcing, Rocky Mountain J. Math.

  Volume 32, Number 4 (2002), 1071-1100. (Euclid)

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

In terms of classifying toposes

On the interpretation of forcing via classifying toposes (see also at Kripke-Joyal semantics):

• William Lawvere, p. 5 of: Quantifiers and sheaves, Actes, Congrès intern, math., 1970. Tome 1, p. 329 à 334 (pdf)

• Myles Tierney, Forcing Topologies and Classifying Topoi, pages 211-219 in: Alex Heller, Myles Tierney (eds.) Algebra, Topology, and Category Theory: A Collection of Papers in Honor of Samuel Eilenberg, Academic Press 1976 (doi:10.1016/C2013-0-10841-0)

• Michael Makkai, Gonzalo Reyes, First Order Categorical Logic, Lecture Notes in Mathematics Volume 611, Springer 1977 (doi:10.1007/BFb0066201)

• Peter Johnstone, pages 270, 273, 348, 353 of: Topos theory, London Math. Soc. Monographs 10, Acad. Press 1977, xxiii+367 pp. (Available as Dover Reprint, Mineola 2014)

• Andreas Blass, Andrej Ščedrov, Classifying topoi and finite forcing, Journal of Pure and Applied Algebra 28 (1983) 111-140 [doi:10.1016/0022-4049(83)90085-3]

• Andrej Ščedrov, Forcing and classifying topoi, Memoirs of the American Mathematical Society (1984) [AMS:memo-48-295]

• J. Benavides, The logic of sheaves, sheaf forcing and the independence of the Continuum Hypothesis (arXiv:1111.5854)

• David Roberts, Class forcing and topos theory, talk at Topos at l’IHES 2015 (talk notes, video recording)

• Mike Shulman, Answer to ‘A better way to explain forcing?’, (MathOverflow)

On Scedrov 84, Peter Johnstone writes in his review (The Journal of Symbolic Logic Vol. 50, No. 3 (Sep., 1985), pp. 852-85):

Until recently, logicians could have been forgiven for treating topos theory as a closed book, whose applications to logic (however interesting they might appear from the outside) were accessible only to insiders well schooled in the mysteries of category theory $[...]$ $[$ Ščedrov’s book makes $]$ a very clear case for the advantages of the topos-theoretic approach to forcing namely, that it provides a clear conceptual view of what generic structures really are, as well as a workable mean $[...]$ Although categorical ideas and terminology are inevitably present, they are handled so skilfully that the categoriphobic reader need have few qualms about them $[...]$ Ščedrov’s work ought to go a long way towards demolishing the wall of incomprehension that has hitherto prevented many logicians from appreciating what topos theory has to offer their subject.