Suppose is a forcing notion in some model of , and let be a -generic filter over . Then there are a few properties a can have that are especially useful.
Adding reals: A lot of forcing notions add reals to the ground model in some form or another. Prominent examples would be Cohen reals for Cohen forcing, Sacks reals for Sacks forcing, etc. However forcing with doesn’t only add a single -real, as reals definable trough that new real also get added. Hence it would be lovely to have a few properties that describe general reals added by forcing notions. Examples of such properties are:
- Adding dominating reals: In every forcing extension , there is a real that dominates .
- Adding unbounded reals: In every forcing extension , there is a real that is not bounded by any real in the base model.
- Adding splitting reals: In every forcing extension , there is a real that splits any real in the base model, i.e.
It turns out that if adds a dominating real, it also adds both unbounded reals (this is easy) as well as splitting reals (this is not). However none of these inclusions are reversible as shown by the following table, exposing which forcing notions add which types of reals:
|Notion||Dominating reals||Unbounded reals||Splitting reals|
Chain conditions: Let be a regular cardinal. We say that satisfies the -chain condition, if every maximal antichain in has size strictly less than . The case is also called the countable chain condition or ccc for short. This condition is useful since we have the following
Proposition: If satisfies the -chain condition, then all the cardinals are preserved in any forcing extension with .
This essentially follows from the fact that if we have a surjective function for some cardinals in the extension, we also have a -name for it. Then for the set :
is an antichain in , and hence of cardinality strictly smaller than . Now this set consists of all the conditions above which the value of will eventually be forced to be some value . Since , we know that number the possible choices for must also be , since every such choice has to be forced by some condition in the filter, by the fundamental theorem of forcing. By the defineability of forcing, we can define another surjective function in the base model:
where the parameter is used to sweep all the possible choices of . Hence for this implies that
So that also in the base model. If then if we would have by regularity of :
A contradiction to the surjectivity of . Hence in both cases, cardinals are preserved.
Closedness Properties: Let be any cardinal. Then is called -closed , if for any ascending sequence of conditions there is a condition such that for all . For , this is called -closedness. This property complements the -chain condition, in that the following hols:
Proposition: If satisfies the -closedness condition, then all the cardinals are preserved in any forcing extension with .
This follows from the fact, that if is a function in with , then is already in the ground-model. Hence no cardinals less than can be collapsed. Now why is this the case? has a -name in . Start with any condition . Define the condition by:
for some . This is possible, since the conditions that define are open dense in . Again by open density find such that for some with:
Continue in this manner to obtain an ascending sequence . Now at the limit stage, utilize the -closedness to find for any . Continue this process further until we have a condition such that for all :
So above each , there is a which essentially says that is definable in , hence no matter which generic filter we choose, there will be some , and hence is already a function in .
Properness: A generalization of the . Remember that assures that no uncountable cardinals get collapsed. Also gets preserved under finite support iterations. However this is often too much to ask from a forcing notion, hence the notion of properness, for which the following hold:
Proposition 1: If is proper, then it does not collapse .
Proposition 2: If is a countable support iteration of , and for each we have , then is proper.
Proposition 3: If is a countable support iteration of proper forcing notions which satisfy one of the following properties
- Laver Property
- Preservation of P-points
Then is proper and has the respective property.
So now to the definition of properness. For a regular limit cardinal let:
These are all the sets which are hereditarily of cardinality . It turns out is a model of minus the power set axiom. For the definition of properness, we need large enough. Assume in the following, this will suffice. Let be an elementary submodel of , i.e. any statement about elements of is true in iff the corresponding statement (where all the quantifiers have to be relativised) is true in .
Let . We say that is -generic if it has the following property: If and . So if the model says that a subset is open dense, should intersect it, similarly to genericity over . Next, a condition , which does not need to be in , is -generic if
where is the canonical -name for the -generic filter in .
Finally, a forcing notion is called proper, if for all countable elementary submodels of which contain , and every condition , there is a -generic condition .
Laver Property: A property that makes sure no Cohen reals are added while forcing. Let be the family of all function , such that . The family is restricting the growth of its member to exponential growth. A forcing notion is said to have the Laver property, if for any function in the ground model and any -name of a function , such that we have:
Another way of looking at the Laver property is that if satisfies the Laver property, the models and cannot be too wildly different, since each bounded funtion in the extended model can at least be approximated in the ground model.
Preserving P-points: Let be a P-point in . Then we say that preserves , if generates an ultrafilter in any extension. Equivalently:
Note, that we don’t require the ultrafilter generated in the extension to be a P-point. This is where the following statement comes in:
Proposition: Let be a proper forcing notion and be a P-point in the ground model . If the filter generated in is an ultrafilter, then it is a P-point.
So nice enough forcing notions maintain P-points in this stronger sense.
Furthermore, the countable support iterations of P-point preserving proper forcing notions also preserves P-points.
-bounding: A forcing notion is called -bounding if there are no unbounded reals in any forcing extension.
-boundedness of proper forcing notions is preserved under countable support iterations.