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.
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.
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.
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.
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.
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.
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.
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 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.
Exposition is in
Another good introduction is in Schoenfield 71
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
Discussion of the interpretation of forcing as the passage to classifying toposes includes
Michael Makkai, Gonzalo Reyes, First Order Categorical Logic, Lecture Notes in Mathematics Volume 611, Springer 1977
Andrej Skedrov, Forcing and classifying topoi, Memoirs of the American Mathematical Society 1984; 93 pp
Andreas Blass, Andrej Skedrov, Classifying topoi and finite forcing (pdf)
David Roberts, Class forcing and topos theory, talk at Topos at l’IHES 2015 (talk notes pdf, video recording)
On Skedrov 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 $[...]$ $[$ Skedrov’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 $[...]$ Skedrov’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.