This post continues the previous one. As before, I’m following the presentation from Gitik’s Handbook chapter, none of the results here are mine, and any mistakes are my fault.

Now that we’ve defined the long extender forcing, we want to prove the following theorem:

Theorem (Gitik) : Assume GCH holds in , and let be an increasing sequence of -strong cardinals with and , and let be the corresponding long extender forcing. If is -generic for , then the following hold in :

- No New bounded subsets of are added;
- All cardinals are preserved;
- ;
- In particular, since GCH holds in the ground model, we have that GCH first fails at .

We will proceed by first showing that satisfies the chain condition. From there, we will black box a rather technical lemma for later, but use this technical lemma to show that forcing with preserves and adds no new bounded subsets of . Finally, we will show that -many sequences are added to . In order to show that satisfies the -chain condition, we will heavily abuse the fact that the forcings are basically Cohen forcing.

We begin by fixing some terminology. Letting , we call the stem of and the rest of the condition the tail of . Next recall the three lemmas about the extender ordering (as they will be abused quite a bit) in the form that we’ll be using them:

Lemma 1: (GCH) Fix , and . If is a collection of ordinals below , then there are -many such that for each . In particular, is -directed.

Lemma 2: Suppose that is a collection of ordinals with for each . If for each , then .

Lemma 3: Suppose that is a collection of ordinals with such that for each , then there is some such that, for each , .

Lemma : satisfies the chain condition.

Proof: Let be a collection of conditions from with and for . We begin by noting that we can refine our collection of conditions to a collection of size with the property that for each . Furthermore, since is a collection of partial functions from to of size and GCH holds in the ground model, we can further refine to a collection with the following properties:

- For each , the collection forms a -system with root such that for each .
- For each , the collection forms a -system with root such that , and for each .

Our next step is to show that, given any , there is a condition (directly) extending both and . That the extension is direct is more an artifact of the proof, and not in and of itself important. We begin by fixing such , and note that we can easily construct for by setting since they both agree on the root of the -system. Constructing for is only slightly harder, as we need to make sure that each portion of the condition agrees with the others.

We construct as before. We would like to construct in the same fashion, but we need to make sure that has a -maximal element, and that said maximal element doesn’t get into the domain of . This is easy though, as Lemma 1 guarantees that there is some with such that it -dominates every element of . With this in mind, let , and note that our choice of is completely decided by our choice of . That is, let , and use Lemma 2 and Lemma 3 to shrink to satisfying the conclusions of said lemma for . Then by construction , and note that we can slightly change each by adding finitely many elements to make sure that for . Thus is a condition directly extending both and and hence we have shown that has no anti-chains of length .

At this point, we would like to show that satisfies the Prikry condition. In order to do this, we will go through a version of the strong Prikry lemma for this forcing, as it will allow us to show that is preserved in the extension. Before doing this, we need to figure out what it means to take an -step extension of the stem of a condition. So, let with for . For , we define the -step extension of the stem of by to be the condition defined as

.

As before, . From our prior discussion, we’re basically replacing the first terms of past the stem with the minimal extensions (in the order) by Cohen conditions agreeing with . With this in hand we have an idea of what the strong Prikry lemma should state:

Lemma: Let , and let be dense open in . Then there is some and such that every -step extension of lands in . That is, for every , we have that .

The proof of this lemma is rather technical, so I’ll hold off on the proof of this until the next entry. For now, the plan is to use the above lemma to finish showing that no new bounded subsets of are added, and that is preserved in the extension.

Lemma: satisfies the Prikry condition. That is, for every condition , and every sentence in the forcing language$, there is some such that decides .

Proof: Let be a condition and a sentence in the forcing language, and let . Using the strong Prikry lemma, we can find a and be such that every -step extension of lands in . Let with for the sake of simplifying notation. Our goal is to show that we can refine to a further direct extension that lands in . In order to do this, we will simply refine the measure one sets in the tail of so that it only allows for step extensions that all decide in the same way. But then, given any -step extension of , we see that all non-direct extensions will decide in the same way. So, each -step extension will decide in the same way, and we can continue going backwards until we see that itself actually decided . For the sake of simplicity we will assume that , since this case is demonstrative of how the refining process works, and the indexing gets way too annoying for arbitrary .

So by our assumption, we have for any pair of ordinals with and , that . Fix a faithful enumeration of , and for each , set

, and

.

Let denote whichever one of the above sets ends up in . Next, let , and . Since one of these above sets has measure one, let be whichever one of those two sets ending up in . Finally, set

.

Noting that shrinking the measure one sets in our conditions doesn’t change the fact that they’re still condition, let denote the condition resulting from starting with , and replacing with for . Then by construction we have, for every and every , that decides in the same way. Hence, we see that our reasoning from earlier allows us to conclude that every non-direct extension of decides in the same way and thus so does . This completes the proof.

As usual, now that we’ve seen that satisfies the Prikry condition, we can implement the closure of the tail under the direct extension ordering and show that forcing with adds no new bounded subsets of .

Lemma: Forcing with adds no new bounded subsets of

Proof: We’re going to show that any bounded subset of in the extension is completely decided by one condition, so let , be a name, and be such that and . We will inductively construct a -decreasing sequence of conditions sequence as follows:

- Let ;
- At successor stages, assume that has been defined, and use the Prikry condition to find be such that .
- At limit stages, assume that has been defined for each , and define in the obvious way. For , we simply set and note that since each it still had size at most . For , set . Now set where is above the domain of and -dominates every member of (use the fact that combined with Lemma 1). Finally set using the fact that is complete for , and use Lemma 2 and Lemma 3 (and the fact that ) to shrink to satisfying the conclusions of those lemmas for the collection which has size by construction. Finally set .

Note that, by construction, we have that for each at stage . Now that we have our desired sequence, we can use the limit stage construction on to construct a condition that is a lower bound for the sequence. But by construction, we have that, for all , . Hence is completely decided by a single condition, and so . Since and were arbitrary, it follows that forcing with adds no new bounded subsets of .

All we have left to do is use the strong Prikry lemma to show that is preserved in the extension. One thing to note is that the argument actually generalizes to other Prikry forcings that satisfy the strong Prikry condition. In fact, all of the previous lemmas depended on the fact that the strong Prikry lemma was satisfied, and the tail is sufficiently closed under the direct extension ordering. In other words, once we have the strong Prikry lemma and the chain condition for a Prikry forcing over , we’ve successfully shown that cardinals are preserved in the extension, and no new bounded subsets of are added. This observation allows for replacing the extenders that we’re using with shorter ones.

So why try to use shorter extenders? On one hand, we would weaken the consistency strength of the assumptions used, but that’s not a huge deal for us. The problem with using long extenders is that it prevents us from collapsing to any sufficiently small cardinal such as . What we would like to do is weave collapses into our Prikry forcing in order to simultaneously blow up the power of while collapsing it to . This turns out to be difficult since Prikry sequences eventually end up in the measures we have lying around (this follows form standard density arguments) and are therefore form a collection of indiscernibles for . So in order to collapse , we want our collapses to miss the indiscernibles, which doesn’t allow for much collapsing when using long extenders. So, if we shorten the length of the extenders, we will actually shrink the intervals in which indiscernibles appear. If we can sufficiently shrink these intervals, we can collapse down as far as . Anyway, we now show that forcing with preserves .

Lemma : Forcing with preserves .

Proof : Suppose otherwise, and note that in the extension, will be below . Work in , and let , be a name, and be a condition with and such that “ has unbounded range. We will use the strong Prikry lemma, along with the fact that to manufacture a bound on the range of . For each , let

.

We now use the strong Prikry lemma to inductively define a -decreasing sequence as follows:

- Set ;
- At successor stages, assume that has been defined and use the strong Prikry lemma to find and such that every -step extension of the stem of ends up in .
- At limit stages, use the construction from the previous lemma to obtain a lower bound for .

Let be a lower bound for the sequence , and note that for each , there is some such that every -step extension of the stem of decides the value of . For each , define

.

Since , we see that the above supremum is over at most ordinals . Thus, since is regular in the ground model, , and thus . Finally, set , and note that we have by construction

.

But and forces that the range of is unbounded in , giving us a contradiction.

We are now a few density arguments away from proving the following:

Theorem (Gitik) : Assume GCH holds in , and let be an increasing sequence of -strong cardinals with and , and let be the corresponding long extender forcing. If is -generic for , then the following hold in :

- No New bounded subsets of are added;
- All cardinals are preserved;
- ;
- In particular, since GCH holds in the ground model, we have that GCH first fails at .

Proof: We’ve already shown 1 and 2, and 4 will follow immediately once we prove 3. So, let be -generic for . Let , and define a function by setting if and only if there is some with and such that . By genericity, is defined on all of . Using these functions, we define for each the sequence , noting that for each . Now, it might turn out that a good chunk of these sequences come from the ground model, since they could be that they are determined completely by a single condition. However, the following claim will give us that the set has size :

Claim: If , then there is some with such that for each .

Proof (of claim): What we want to show is that for a large enough , such that for every , we can find a condition such that, for every where , both and are in . If we can do this it follows that for each , we have . Thus, it follows that for all , by definition of the ordering.

So, we work in and let with for each . We will attempt to extend to a condition as above. We begin by picking some , and noting that we can generically extend to a condition with for each where . Do the same to extend to with replaced by to get the desired condition. This completes the proof of the lemma.

The only thing left to prove is the strong Prikry lemma, and we will have proved that the long extender forcing does what it was supposed to do. As I mentioned earlier, the proof is rather technical, so I will save it for the next entry by itself since I should work through it fully anyway.