First, some definitions to add context to the post. Throughout, we will assume that is a set of regular cardinals with no maximum such that .
Definition: For , we say that is a generator for if is the ideal generated from by adding in . In this case, we write . If is a generator for , we write for to indicate this.
The key component of Shelah’s celebrated ZFC bound on is not only that generators exist for every , but that we can manufacture transitive generators for large enough portions of .
Definition: Suppose that , then a sequence of generators is transitive if for every .
The construction of transitive generators from the Abaraham-Magidor chapter of the Handbook uses something called elevated sequences to get transitive generators. While this ends up being quite slick, the construction from Sh430 is more transparent. The basic idea is to shove everything into small elementary submodels, and then try to make your generators transitive. Because this procedure can be carried out in small elementary submodels, we know that this has to stabilize eventually. The only problem now is checking that what we end up with is still a sequence of generators. This is done by defining functions which behave like universal cofinal sequences, and using these functions to then show that the objects we end up with are generators.
Now, the Abraham-Magidor approach turns the above approach on its head. The elevated arrays play the part of functions which look like universal cofinal sequences, and these are used to define transitive generators. This ends up looking nicer, if a bit mystifying. Both proofs share many of the same characteristics though, including the key use of characteristic functions of -approximating sequences of elementary submodels.
As I’m interested in where the Abraham-Magidor approach diverges from Shelah’s approach, I’m going to pick up where this happens.
First let where each $\vec f^\lambda$ is a universal cofinal sequence which is minimally club obedient at cofinality for each regular such that . Now, let be regular with , and fix a -approximating sequence of elementary submodels of some with . That is:
1) Each ;
2) for each , we have that ;
3) for every ;
4) is an initial segment of .
Set . For each and , we define
We can then find a club such that, for each in and , the following hold:
- is a generating set;
We’re also going to ask that , so . One thing to note here is that I’m probably being overly careful in the sense that we probably don’t need that . I just know for sure that the above works if we give ourselves a little more room, and peeling off a few cardinals at the beginning of won’t effect anything. The above list of results can be derived from the results in Section 5 of the Abraham-Magidor paper. Now we’ve reached the point where the two approaches to transitive generators differ. As I said before, we’re just going to make these generators transitive by brute force, and then prove that the brute force approach didn’t break anything. So we fix in and , and define the following sets by induction on :
- At successor stages, we set
- At limit stages, we set .
The notation might look horrible, but really we’re just starting with the set and attempting to make it transitive at successor stages. At limit stages, we simply take the union. The nice part is that this entire procedure (for fixed ) can be carried out inside which has cardinality . As the above sequence of sets is increasing and continuous in , and is a sequence of length , it follows that this sequence has to stabilize at some point. Let’s call this stabilization point as this depends on all three parameters.
Now, note that , and so there must be a single that works for each . So now we have the following properties of our sequence :
- The sequence is transitive;
- for each , we have that .
The first gives us transitivity, and the second gives us that the ideal contains . All we have to do now is show that , as that will tell us that won’t add the wrong sets. Along these lines, for each , and for each define an increasing sequence of functions with domain by induction on as follows:
- At limit stages, we simply set .
- At successor stages, we define based on how found its way into . We have two cases: either it was in already, or it was in some for .Case 1: If , then we let .
Case 2: Suppose that the above case fails, but such that where is minimal. Then we set .
By construction, we see that this sequence is increasing and that the domains of the functions is as desired. Note that we suppressed any reference to , but this entire construction can be carried out inside . Finally, for every and every , we have that . This follows readily from our construction.
At this point, we’re ready to finish the proof. The idea is that the functions we built look enough like universal cofinal sequences, that we can use them to show we have generators. To this end, we suppose that . This means that we can find some which serves as a -upper bound for , since is directed. The fact that we can find such a in follows from elementarity along with the fact that the sequence ends up in . Here’s the kicker, though: since and , it follows that which is a contradiction. So we have transitive generators.