The Forcing Theorem

Let be a countable Transitive Model and a Forcing Partial Order. Then there is an Absolute Forcing Relation on .

Proof (chunky one)

Definition of

We first define the Forcing Relation on atomic formulas. From the definition of the Forcing Relation, we want precisely when some has . Note that iff and for some . But then also iff some has .

We conclude that iff any filter containing has some with and with . It is then convenient to look at

If this set is Dense Below , then any filter containing will intersect it. This gives us a and thus also some . From we find that and from we find and thus .

To define we use this idea along with Axiom of Extensionality. Say that if and only if

is dense below for all . Then if and only if

This is now enough to give a recursive definition on the rank of Names. This wraps up the atomic formulas. For composites, we have the following definition:

By the lemmas about Dense Below, we can show that is downwards closed. Furthermore, one can check that this definition is Absolute for .

Properties

Let be a -Generic Filter over . To find that is a Forcing Relation, we need to show that:

We shall first prove this for atomic , which boils down to the following two equivalences

We prove these by induction on terms. Then we prove it for non-atomic by induction on formula complexity. These will together imply that is a Forcing Relation.

Claim 1

Proof

By -induction.

Suppose forces . Fix . Then there is some with . As is a Filter, there is some . By assumption, is Dense Below , and so also below . But then one finds some with . By definition of and from , we find with . As , by induction hypothesis find . Also so and thus so .

Fix and suppose that some is not dense below i.e. that doesn’t force . Then for some and all we have

In particular, and for any and any

Suppose that some . From and we find that . Also and thus as above. We conclude that and are Incompatible here and thus

Call this sentence and let be

Define the set

For any , either is always dense below , in which case so , or there is some with , by previous analysis. We conclude that is dense so there is some . Assume that and thus find with and for any and any with we have . Then so so , so there is some with and . By induction hypothesis, there is some with . But then there is some with , and we get . Then by above which is a contradiction as they are both in . We conclude that is false so . This completes the proof.

Claim 2

Assuming The Forcing Theorem > Claim 1:

Proof

By -induction.

Assume . Thus find some with and . By The Forcing Theorem > Claim 1, find such that . Then find in . Note that any has and so

is Dense Below and thus and .

Suppose some for some . Then (as above) is Dense Below . Thus find and with and . Then so . Also by The Forcing Theorem > Claim 1 and we find so .

Claim 3

If satisfies the Forcing Relation property for and then so it does for .

Claim 4

If satisfies the Forcing Relation property for then so it does for .

Proof

Assume

We want to show:

Consider

By definition of , this set is Dense. Thus find some . By assumption it follows that

so by the induction hypothesis . But then by definition .

Suppose and . Assume that (towards a contradiction) By induction hypothesis, find such that . Then find some with . Now by definition of , we have . But also so (by downwards closure of ). This is a contradiction.

Claim 5

If satisfies the Forcing Relation property for then so it does for .

Proof

Assume that . Thus take some with . Then for some . Then there is some with . Thus any has . We have proved for all and thus .

Assume that for some . Then

is dense below . Thus there is some and with . By assumption, then . But then so we are done.