Model Extension

Let be a Transitive Model. Let be a Forcing Partial Order. Let . Then the model extension of by is

where are the -Names.

Theorem

Let be a (countable) Transitive Model of Let be a Forcing Partial Order. Let be a -Generic Filter over with . Then is a (countable) Transitive Model of and furthermore, and .

Note

The above statement can be modified to conclude the following: If is finite, then there is some finite such that if is a countable Transitive Model of Then is a countable Transitive Model of and furthermore, and .

Proof

Firstly, if is countable, then so is . But so it is also countable.

By definition, it is also a Transitive set. Secondly, we know that and from Canonical Names.

Any Transitive Model satisfies Axiom of Extensionality and Axiom of Foundation. Furthermore, as , then satisfies Axiom of Infinity.

Pair

Pair-set axiom Given , we need a Name for

Set

as the obvious name for the pair. Then clearly:

because .

Union

Union axiom Given need a Name for

Define

As is a Filter, we can check that:

Separation

Axiom of Separation Let for some . Let be a formula with one free variable (we omit the parameters for readability) Want to find a Name for

Set

where is the Forcing Relation given by The Forcing Theorem. Then we claim that

Suppose .

Take such . As is a Filter Base there is some such that . From we conclude . Now we can write

Thus by definition. Also , so by definition of value of a Name, we have

which completes this direction.

Suppose

Powerset

Powerset Axiom Fix . Using define:

We claim the following:

As we already have Axiom of Separation in , we can then separate the powerset from

Proof of claim

Let and . Set

Then one can show (Example sheet 3) that

Also clearly so we are done.

Replacement

Axiom of Replacement Let and be a Function Class (in ). By Axiom of Separation it is enough to show that there is some such that

(where we omit the parameters for clarity) In , find such that and write for

(by The Forcing Theorem, this is well defined) Again in , use Lévy Reflection Theorem to find such that is Absolute between and . Define

and set . We now check the above. Let Let such that . By Forcing Relation find such that

It follows that

By Absoluteness we have

so there is some such that

from where it follows that

But is a Function Class so certainly

Thus we conclude so .

Choice

Suppose Axiom of Choice holds in . Suppose

By Axiom of Choice in , find an injection

so is Well-ordered.