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: .
Definition: .
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.