Let be a Forcing Partial Order. Let be an Ordinal and let be a collection of Strong Antichains. Define

We say that a Name is a nice name if for some .

Lemma

Let and assume that has -Chain Condition. Then there are at most

nice names for subsets of .

Proof

Each Strong Antichain in has at most elements, so there are at most antichains. But then there are at most families of antichains, so at most that many nice names.

Theorem

Let be a -Generic Filter over a Transitive Model . Then every subset of in has a nice name in .

Proof

Fix for some Name . Suppose that is not a nice name. Fix . Then if and only if some forces . Using Zorn’s Lemma in , build a maximal Strong Antichain . Thus we find

We now prove that

which will finish the proof as is a nice name.

If then by definition there is such that

We conclude that so . Thus .

If , by Forcing Relation find

By the lemma in Dense Below, if then there is some with for all . So find with . Then is a larger antichain with . Therefore, we could have WLOG taken . But then so

Corollary

If and

then define to be such that

Then the Model Extension has:

Proof

Every subset of in has a Nice Name in . Also there are at most Nice Names in .