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 |
Mathias | ✔ | ✔ | ✔ |
Cohen | ✘ | ✔ | ✔ |
Sacks | ✘ | ✘ | ✘ |
Silver-like | ✘ | ✘ | ✔ |
Miller | ✘ | ✔ | ✘ |
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
-boundedness
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.