Envelope forcing
In a recent paper (Corduan–Dorais 2012), Jared Corduan and I considered various notions of combinatorial indecomposability for finite ordinal powers of In this process, we uncovered two weak forms of Ramsey’s theorem for pairs ():
 The Weak Ramsey Theorem ().
 For every coloring there are a color and an infinite set such that is infinite for every
 The HyperWeak Ramsey Theorem ().
 For every coloring there are a color and an increasing function such that is infinite for every
The first is equivalent to what we called the game indecomposability of the ordinal and the second is related to the lexicographic indecomposability of You can find out more about these notions of indecomposability in our paper, what I want to write about here is the forcing technique that we used to show that is conservative over with induction and to separate the two principles and I’ve been calling the method envelope forcing since the basic idea is to force over a larger model that envelops the original one rather than forcing over the ground model itself. In the following, I will give a brief tour of this method, skipping all the gory details (that can be found in our paper).
The forcing for is a twist on Cohen forcing. Given a coloring we want to generically add an increasing function such that the sets
are all cofinite (and hence infinite). Obviously, we can’t do this for every coloring so we will only consider coloring for which there is no increasing function such that the sets
are all infinite. The obvious idea is to force with the poset that consists of all finite functions such that the sets
are cofinite when This is just another variant of Cohen forcing, which is well understood, so we should be all set! Unfortunately, this is not the case since this poset has a definition so our ground model so we will have a very hard time understanding forcing with from inside The trick to get around this issue is to force over an envelope model where has a more manageable definition.
So we start with a ground model of The fact that satisfies guarantees that the extension obtained by adding all sets that are definable over satisfies In the poset described above has a definition, so there is no trouble forcing with and thereby adding a generic function that does make all the sets
cofinite. Of course, adding to is of no use, we want to add to the ground model We can certainly form the model obtained by adding to and closing under comprehension. The result will certainly be a model of because but we also want to satisfy so we can iterate this process and obtain a model of in the limit.
It turns out that is relatively large in the poset of all finite increasing functions — which is just a variation of Cohen forcing for our base model The following lemma (corresponding to Lemma 3.10 in (Corduan–Dorais 2012)) shows that the generic for over is also somewhat generic for over the original model sufficiently generic that the extension will satisfy
Relative Largeness Lemma. Suppose is definable over For every if for every there is a (in but not necessarily in ) such that then for every there is a such that
In particular, if is dense below in then is dense below in Therefore, is generic for over :
For every which is definable in there is a that either or has no extension in at all.
Note that is unlikely to be much more generic than that since no initial segment of lies in which could be dense in for a suitable coloring Nevertheless, just generic enough to ensure that satisfies More precisely, relative largeness ensures that is low over the ground model:
Lowness Lemma. Every formula with parameters in is equivalent to a formula with parameters in
The reason for this is that contains Skolem functions for formulas with parameters in (CorduanDorais 2012, Proposition 3.13). Once Skolemized, a formula becomes Because satisfies and is an extension of it follows that satisfies So now we can iterate this process externally, taking care of any coloring that appears along the way, to obtain a model of
Is this envelope forcing technique useful for anything else? Yes! In fact, the method was inspired by Hirschfeldt and Shore (2007), who used a similar technique for and (The main differences are that they use methods from computability theory and they mostly care about models, so they have no need for enveloping models.) Let’s see how to recast these two examples in terms of envelope forcing.
Recall that a (countable) linear ordering is stable if every element either has finitely many predecessors or has finitely many successors. Finite linear orderings are stable, and so are the infinite linear orderings and The principle says that these are the only stable linear orderings, which boils down to saying that every infinite stable linear ordering has an infinite ascending or descending sequence. This is not provable in but it is conservative over as can be shown by an envelope forcing argument.
The forcing for the infinite stable linear ordering consists of all finite increasing sequences of elements of such that has only finitely many predecessors in Note that is definable over the ground model, so we are in a very similar situation to the above. Hirschfeldt and Shore observed that if has no infinite descending sequence, then is relatively large in the partial order of all finite increasing sequences of elements of It then follows that an envelope generic for is necessarily low over the ground model and we can generically add an increasing sequence to without destroying
It turns out that implies but the relationship between and is unknown. The methods that Hirschfeldt and Shore used for can also be recast in terms of envelope forcing. However, rather than doing that, I will present another application of envelope forcing that incidentally forces
 The Path Ramsey Theorem ().
 For every coloring there are a color and an increasing function such that for all (a homogeneous path).
As usual, the Stable Increasing Path Ramsey Theorem () is the restriction of to stable colorings, i.e., colorings such that exists for every
Note that directly implies The following asymmetric strengthening of directly implies
 The Stable Mixed Ramsey Theorem ().
 For every stable coloring either there is an infinite homogeneous set, or an infinite homogeneous path.
The technique of envelope forcing can be used to show that is conservative over The natural forcing to add a homogeneous path for a stable coloring consists of all finite homogeneous paths such that Indeed, this condition on guarantees that the path can be continued further, provided that there are infinitely many such that (If there are only finitely many such it is easy to construct an infinite homogeneous set.) It turns out that if has no infinite homogeneous set in then is relatively large in the partial order of all finite homogeneous paths for
To see this, suppose is definable over the ground model Suppose further is such that for every there is an (in but not necessarily in ) such that Finally, for the sake of contradiction, suppose that is an element of that has no extension in Since there are infinitely many such that too. So, by an effective search, we can find an infinite sequence of extensions of in (in but not in ) such that the tips enumerate an infinite set in increasing order. Since has no extension in we must have that for every But then it is easy to recursively construct an infinite homogeneous subset of which contradicts the fact that there are no such sets in
It follows that is conservative over hence so are all of its consequences and However, this does not separate any of these principles from or even To do this, we need to recast the forcing arguments into the language of computability theory. The argument for gives the following.
Theorem. If is a computable coloring, then one of the following is true:
 There is a computable increasing function such that is infinite for every
 There is a computable generic increasing function such that is cofinite for every
It was shown by Downey, Hirschfeldt, Lempp and Solomon (2001) that some computable instances of have no low solutions. Since follows from this shows that there is an instance of that has no low solutions either. A computable generic function is always low, so there is an model of that contains only low sets. This model cannot be a model of which shows that does not imply
The argument for gives the following.
Theorem. If is a stable computable coloring, then one of the following is true:
 There is a computable increasing function such that for all
 There is a computable generic increasing function such that for all
So does not imply Neither do any of its consequences, such as and
References

J. R. Corduan, F. G. Dorais, 2012: On the indecomposability of $\omega^n$, Notre Dame J. Formal Logic 53, no. 3, 373–395.

mr: 2981014

zbl: 1260.03017

arxiv: 1111.1367


R. Downey, D. R. Hirschfeldt, S. Lempp, R. Solomon, 2001: A $\Delta^0_2$ set with no infinite low subset in either it or its complement, J. Symbolic Logic 66, no. 3, 1371–1381.

mr: 1856748

zbl: 0990.03046

doi: 10.2307/2695113


D. R. Hirschfeldt, R. A. Shore, 2007: Combinatorial principles weaker than Ramsey’s theorem for pairs, J. Symbolic Logic 72, no. 1, 171–206.

mr: 2298478

zbl: 1118.03055

Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.
Comments

François G. Dorais wrote
The statement of the Relative Largeness Lemma has been corrected after Paul Shafer kindly reported an error.

François G. Dorais wrote
Updated references.