: q is in dom(x) and r ||- "q is in z"}. By definition, dom(z') is a subset of dom(x). What is val(z',G)? Well, this is determined by which "tags" are in G. But note that by the definition of forcing, if r is in G, then val(q,G) is in val(z,G) = Z. Therefore, val(z',G) is a subset of Z. This is progress, but what we really want is for val(z',G) to be actually equal to Z, and this is not at all clear. What we need in order to prove val(z',G) = Z is that for every Q in Z, there is a P-name q of Q in dom(x) and a P-name r in G such that r ||- "q is in z." Finding a suitable q turns out not to be that hard, but the existence of r is not so clear; what we need is a theorem that for every statement phi (such as "Q is in Z") that is actually true in M[G] for a particular G, there is some element r of that particular G such that merely knowing that r is in G is enough to deduce that phi is true of G. This doesn't seem plausible. In general, knowing just one element of G doesn't tell us very much about G. However, we can fix this problem if we restrict G and P to have a certain structure, so that some elements r of G are "more informative" than others, i.e., knowing that r is in G tells us more about G than knowing that some other element p is in G. The simplest way to achieve this is to impose a partial ordering < on P (with "1" being the unique maximal element) and to require G to be a *filter*, i.e., for G to have the following two properties: 1. If r is in G and r <= p then p is also in G. 2. For every p and q in G there exists r in G such that r <= p and r <= q. The first of these conditions ensures that knowing that some element r is in G tells us not only that r is in G but that every element >= r is also in G. Thus, r is "more informative" than p if r <= p. The second condition may be thought of as capturing the idea that for any two elements p and q, there is some element r that is at least as informative as p and q put together. If we are going to insist on looking at only single elements of G to get information about G, then this is clearly a useful condition to impose. If we now revise our definition of ||- by inserting the technical conditions that P be a partially ordered set and G be a filter, then this gives us more hope of being able to find r in G such that r ||- "Q is in Z." Unfortunately, even the condition of being a filter turns out not to be quite good enough. Intuitively, the reason is that since P may be infinite, there is no guarantee that, for an arbitrary statement phi that asserts something about G, there will exist an r in G that will give us enough information to decide phi. We might try finding smaller and smaller r's in the partial order that give us more and more information but we might never find one that tells us what we need to know. The following condition on G solves this problem. Define a subset D of P to be "dense" if for every p in P there exists q in D such that q <= p. A filter G is "generic" if it intersects every dense subset. It can now be proved that if we require P to be a partially ordered set with unique maximal element 1 and we define "p ||- phi" to mean that for all generic filters G in P, phi is true in M[G], then the following is true: Forcing Fact 1. Fix a particular generic filter G of P. Then for any phi that is true in M[G], there exists r in G such that r ||- phi. If we now go back to our attempt to prove the Powerset Axiom, we see that Forcing Fact 1 is just what we need to prove that val(z',G) = Z. The only thing left to prove is that z' is actually in M. For this, one needs the following: Forcing Fact 2. ||- is definable in M. I won't say precisely what Forcing Fact 2 means, but intuitively it asserts that even when we add the side conditions (partial order, generic filter), the definition of ||- is still sufficiently "general" that it does not require any specific knowledge of G; therefore, sets like z' that are defined using ||- still lie inside M. Proving Forcing Facts 1 and 2 is not easy, even after all the above definitions (which themselves are not easy to come up with!) have been provided. Here I must refer you to a Kunen's book for details. The work required to prove them, however, pays off great dividends. Not only Powerset, but all the other axioms of ZFC, can be proved to be true in M[G], using just the two Forcing Facts (without ever having to delve into the proof of the Facts themselves), and following a similar pattern to our proof of Powerset. The Fundamental Theorem is therefore proved! For convenience, we restate it with all the blanks filled in. Fundamental Theorem. If M is a c.t.m., P is a partially ordered set in M with unique maximum element 1, and G is a nonempty generic filter of P, then the set M[G] = {val(x,G) : x is a P-name in M} is also a c.t.m. 6. ~CH revisited Let's see how to apply the Fundamental Theorem to the continuum hypothesis. One's first thought might be to take P to be the set of all ordered pairswith x in k x omega and y in 2, hoping that G can be chosen to be a function from k x omega to 2. However, this does not quite work because the members of a function are ordered pairs, and no particular ordered pair is "more informative" about the function than any other ordered pair. On the other hand, large *subsets* of ordered pairs carry more information than smaller subsets, so this is a hint that we should "pass to the powerset." More precisely, let P be the set of all "finite partial functions" from k x omega into 2, i.e., functions from a finite subset of k x omega into 2. Partially order these functions by reverse inclusion, i.e., f <= g if the set of all ordered pairs in g is contained in the set of all ordered pairs of f. Now it is not hard to see that for each y in k x omega, the set D_y of all elements of P that are defined on y (i.e., that include y as part of their domain) is dense. Therefore, if G is a generic filter in P, G must intersect every such D_y, and the union of all the elements of G will be a *total* function from k x omega to 2. The Fundamental Theorem tells us that we can successfully "insert" this "missing" function into M if it wasn't there already. Furthermore, the fact that G is generic gives us automatically, as a bonus, the fact that each of the k functions from omega to 2 are distinct! (See if you can prove this, by constructing a suitable dense subset in P. You can look up the answer in Kunen.) There is no need to cleverly choose the "right" generic filter; any generic filter will do in this case. Are we done? Well, almost...there are two more points to take care of. First of all, we haven't yet established that generic filters exist. This turns out not to be difficult to prove, but it does hinge on the countability of M (this is where the countability of M turns out to be important). Essentially, because of countability, one can enumerate all the dense subsets, and pick one from each; the filter generated by all these elements will be generic. The second point is more substantial. It is conceivable to me that Cohen could have devised forcing, proved the Fundamental Theorem, and still failed to prove anything new about the continuum hypothesis! The reason is that nothing in the general framework of forcing guarantees that in M[G], the cardinal k will still equal omega_2. Being a cardinal is not an absolute property, so large cardinals can "collapse" into lower ordinals when you pass to M[G]. The reason is that the auxiliary sets in M[G] might include a bijection between k and a smaller cardinal. Luckily for Cohen, though, it can be proved that cardinal collapse does not occur for the particular P described above. See Kunen for details. 7. Epilogue One reason I'm still not totally happy with this exposition is that the definitions "p ||- phi" and "G is a generic filter" still seem to be pulled out of a hat, even though one can get some a posteriori intuition about why each part of the definition is important. There do exist alternative approaches to forcing, e.g., using "Boolean-valued models." This is somewhat more intuitive because the idea that some statements require more "particular information about G" to be decided is encoded "directly," i.e., we take the set of all statements and impose a partial order on this set. The concept of a generic filter becomes simpler (essentially, it becomes an "ultrafilter" in a complete Boolean algebra). However, with this approach one needs to hit on the idea of embedding partial orders in a complete Boolean algebra; I'm not sure how to motivate this. Question for the logicians: are there nice applications of forcing where P is a complete Boolean algebra and no embedding is involved? Another question for the logicians: Say we drop the word "generic" from the definition of forcing, and we say that "p pseudoforces phi" if for every filter G in P, p being in G implies that phi is true in M[G]. Is pseudoforcing definable in M? At first I thought it might be, because it doesn't seem that one needs to know anything about any particular G to decide whether p pseudoforces phi, but Andreas Blass thinks the answer is probably no.