This post is a continuation of the previous one.
As usual, none of the results and proofs are due to me, and I’m still following the presentation from Gitik’s handbook chapter, and Spencer Unger’s notes form the Appalachian Set Theory workshop.
In this post, I will only give the definition of the forcing, and discuss what the forcing is trying to accomplish, and how it’s doing that. Since the forcing itself is rather complicated, I will follow Gitik’s approach and define it in pieces. We begin by fixing , and for each such that , fix a witnessing function with . We now define the th cell as follows:
Set is a partial function from to , and say that if .
Define to be the collection of conditions of the form such that
- , such that contains a -maximal element , and ;
- For if , then for every , ;
- For , if , then for every , .
We say that if
Set , and define the direct extension ordering by . For , we say that if either or and is such that:
- For every , .
We may think of the ordering as the th coordinate of the forcing that we actually want to define when we string all of these blocks together. We should note that, since every condition bottoms out in a Cohen condition, the forcing is actually equivalent to Cohen forcing. Outside of that though, this forcing seems like it will do what we want it to (given the discussion in the previous post). The portions of our conditions give us a set of ordinals of size that have a maximal element in the extender ordering, and cohere well with respect to it, as witnessed by . This will allow us to perform the diagonal Prikry forcing construction at the top elements of these sequences (when we glue everything together) in a nice way. In particular, the Cohen conditions give us a nice way of assigning each element of the sequence to an element of its associated ultrafilter that agrees with the extender ordering and witnessing projections. Finally, rolling up the Cohen conditions along with the parts allows us a way of “predicting” extensions of a condition to a Cohen condition. We will see what is meant by this in the proof of the upcoming lemma.
Of course, for any Cohen condition extending a condition from , its values on the sequence are fully determined by the value at . It turns out that each block is actually a Prikry forcing.
Lemma: satisfies the Prikry condition. That is, for condition and any sentence in the forcing language, there exists some deciding .
Proof : We begin by noting that it suffices to consider extensions of the form since the non-direct and direct extension orderings are the same if is a Cohen condition. The basic idea here is that we will diagonalize against all non-direct extensions deciding , and construct a direct extension that predicts these non-direct extensions. In order to do this, we look at a sort of minimal extension of a condition to a Cohen condition. We first fix a condition and a sentence in the forcing language. Now, for a given , we set
Basically, we take the minimal extension of by a Cohen condition with values decided by . We will now inductively build a decreasing chain of conditions from of length . At each stage, we will find some non-direct extension deciding , and alter the Cohen part of our previous condition so that it predicts this non-direct extension while leaving the first two coordinates of our condition fixed.
We begin by fixing an increasing enumeration of , and set . We first describe what to do at the successor stage of this construction. So suppose that has been defined for some . As we mentioned earlier, we will only focus on altering the Cohen parts of our condition, while keeping the and parts fixed. Let be a non-direct extension of deciding , and set . Define , and note that . Furthermore, note by definition that since , and .
Next, we describe how to proceed at limit stages. So, let be limit and suppose that has been defined for all . Then, we simply set , and note that . Then we define . Now we have a sequence with and such that for . Now define , and note that is still a condition in . Furthermore, we have by construction that and hence decides for each .
The only thing left to do is shrink down so that every extension by decides in the same way. So, we set
Since , it follows that one of these above sets is in , so assume without loss of generality that . Then, every non-direct extension of is below some for some and hence forces . Thus, every non-direct extension of forces and hence so must . This completes the proof.
Definition : We now define the forcing . Conditions are of the form such that:
- Each is a condition in ;
- There is some such that for each , and for each ;
- If , and , then .
We say that if for each , and that if for each .
In the next entry, I want to show that satisfies all of the necessary properties provided that it satisfies the strong Prikry condition. The proof of the strong Prikry condition is rather technical, but I would like to go through it in the last entry in the sequence of entries on the long extender forcing.