A Forcing Partial Order is called -closed if for every and every strictly descending chain

there is some such that

Lemma

Everything is -closed (but that’s not very interesting). However, Finite Function Forcing is not -closed. BUT is -closed.

Proof

First two bits are trivial. For the last bit, let be a descending chain. Set

Then for all .

Theorem

Let be a Model of in which is -closed and . Let be -Generic Filter over and such that . Then .

Proof

Let with . Suppose for contradiction that . Consider

In particular . Let be a name for . By The Forcing Theorem find such that

Define decreasing sequence in . Let . If is a limit ordinal, the fact that is -closed gives us for . Suppose now that is defined and . Since , we find such that

Thus set . This whole definition happens in (doesn’t use ) and so and . Note that function is a function in . By -closure, find for all . But then

which cannot be because (because ).

Corollary

This is a strong preservation theorem: Forcing with can never add a new function . So must remain the same.