Why do we need the comparison lemma?

Question

An inner model is a standard transitive (proper class) structure which satisfies all the axioms of ZFC and contains all the ordinals. The simplest and most well-known inner model is Gödel’s $L$, which is the smallest possible inner model, built by transfinitely iterating the eight basic Gödel operations (or, alternatively, the “definable” or “restricted” powerset). $L$ is the most studied inner model, as it has many combinatorial and fine-structural properties. It admits natural generalisations, $L(A)$ and $L[A]$.

However, by a theorem of Scott, measurable cardinals cannot exist within $L$. So inner model theory is the study of trying to create inner models, which can accommodate large cardinals and have similar structure to $L$. I believe I am close to understanding many of these constructions. However, there are some evidently crucial aspects that I do not quite understand the purpose or necessity of.

From what I’ve read, in all of modern inner model theory, these inner models are built out of “premice”, structures of the form $J_\alpha^A \models \mathrm{ZFC}^-$ (where the $J$-hierarchy is an alternate way of building up the model $L[A]$), which have to have well-founded ultrapowers (in which case they are called mice), and one needs a comparison lemma for establishing which mice are initial segments of (ultrapowers of) each other. This is all well and good, but I have three questions:

• What’s the purpose of building the desired inner model, which is a proper class satisfying all of $\mathrm{ZFC}$, out of set-sized fragments not necessarily satisfying Powerset? Why not directly construe it as $L[A]$? Perhaps I’m misunderstanding.
• What’s the motivation or intuition behind using iterated ultrapowers, and especially, why must our mice have well-founded ones?
• Why do we need to be able to compare the mice which we use to build our model, i.e. why do we need an algorithm for determining whether one mouse is an initial segment of an iterated ultrapower of another?

My expectation is that this is all down to making it easier to prove that the resulting model in fact has fine structure, but I don’t see how. I read some of Steel’s “The Comparison Lemma” in my quest for an answer, and it mentioned that for $L$ the mice are just well-founded structures satisfying a fragment of $\mathrm{ZFC}$ and $V = L$, which was also helpful but the intuition is still nowhere near fully built for me.

Answer 1

If you take a step back and squint your eyes, inner model theory is basically the theory of a big measuring stick that measures the vague notion of "strength of natural set theoretical theories". The marks on the measuring stick are mice (or rather equivalence classes of mice).

Conceptually, it is easier to assume that we live in a rich universe $V$. Let us start with a primitive notion for the strength of a theory: For now, let us measure the strength of a theory $T$, say in a countable language, by finding the least (necessarily countable) ordinal which is not in some wellfounded model of $T$.

Here is a toy example: Consider the theory $T$ in the language $\{\dot \in, \dot +, \dot *\}$ which consists of "everything is an ordinal", "there is an infinite set" and states the usual rules for ordinal addition and multiplication.

The minimal wellfounded model of $T$ is $(\omega^\omega;\in, +, *)$ and so we measure the strength of $T$ to be $\omega^\omega$ as this is the minimal ordinal which does not exists in some wellfounded model of $T$. We now may add a binary function $\dot{\mathrm{exp}}$ to our language and let $T_{\mathrm{exp}}$ add the rules for ordinal exponentiation to $T$. The minimal wellfounded model now becomes $(\varepsilon_0;\in, +, *, \mathrm{exp})$ so that the strength of $T_{\mathrm{exp}}$ is $\varepsilon_0$. In this sense, $T_{\mathrm{exp}}$ is strictly stronger than $T$.

Lets go a bit further: If we consider the theory $T=\mathrm{ZF}+\mathrm{DC}+``\text{all sets of reals are Lebesgue measurable}"$ then we measure the strength of $T$ to be the least ordinal $\alpha$ such that $L_\alpha\models\mathrm{ZFC}+``\text{there is an inaccessible cardinal}"$ (one part of this is due to Solovay, the other due to Shelah). This cannot be expressed naturally as a first order property of $\alpha$ itself, so the natural thing to do here is replace an ordinal $\beta$ on our measuring stick with the structure $L_\beta$. So far this is only a relabeling but these are the first instances of mice.

More generally, as the theories we consider get stronger and more complicated, we really want that this is reflected in our notion of mice. It is crucial, however, that the marks on our measuring stick are still naturally linearly ordered in an unambiguous way, otherwise it would not be a measuring stick. These two properties are at odds with one another and this is a big problem when "effectively" trying to describe the measuring stick further and further.

Our current labeling of ${L_\alpha}'s$ for example stops being effective the latest when we reach the least ordinal $\alpha$ so that no $\beta\geq\alpha$ can be described as the least $\beta'$ with $L_{\beta'}\models T'$ for some $\in$-theory $T'$. This $\alpha$ is exactly $\omega_1^L$, so under $V=L$ the measuring stick is essentially complete. But in our rich universe $V$ (say we have measurable cardinals there and much more), $\alpha$ is countable and very small.

At this point, we need a new notion of mouse and it is not obvious at all how to proceed. It is natural to consider ultrapowers as they are ubiquitous in set theory and since measurable cardinals are easily defined in terms of them and "beyond $L$". I am not sure whether there is a transparent motivation why adding ultrapowers is exactly the right thing to do. Rather, I consider it a deep insight that this can really be implemented nicely. The mice on this next level are the Dodd-Jensen mice and they look like levels of $L$ with ultrafilters thrown inside at the right places.

We should now update the method by which we find the strength of a theory $T$. This is from now on the least mouse which is not in some wellfounded model of $T$. In this step, we did not simply relabel our measuring stick as before! For weak theories we could properly measure before, the two notions agree, but for stronger theories this new notion is much better. (By "measuring properly" I mean that, in some sense, this whole process can be performed without the simplifying assumption of stepping outside into a rich universe $V$).

How do we know now that our measuring stick is still wellordered? The $\subseteq$-ordering will not work anymore, beyond $L$ we immediately get mice $M,N$ neither of which is a subset of the other. Roughly,we now order $M<N$ by "$N$ contains more information than $M$". Remember we put measures on our mice so we should use them! An iterate $M'$ of a mouse $M$ where we did not throw anything away (a "non-dropping" iteration) roughly carries the same amount of information, so $M, M'$ should occupy the same mark on our stick. We now say that $M\leq N$ for mice $M,N$ if there are iterates $M'\subseteq N'$ of $M,N$ so that $M\to M'$ is non-dropping. Sometimes it is necessary that we throw away some stuff along $N\to N'$, but that is fine! This way to compare mice explains a couple of things: First of all, the mice $M,N$ do not just need to be wellfounded themselveses, but as we compare iterates, also the iterates $M', N'$ must be wellfounded (otherwise $M'\subseteq N'$ above would be meaningless). So we must require of our mice that any iteration of them that could be useful for such a comparison must be wellfounded. (Using Shoenflied absoluteness, you can convince yourself that being a mouse cannot be a first order property anymore beyond $L$, so something higher order like iterability is necessary)

For correctness: Sometimes having to throw stuff away in an iteration has to do with the fact that we put partial measures into the mice for technical reasons which are beyond the scope of this answer. I am really talking about a modern interpretation of Dodd-Jensen mice here rather than the original ones.

That this is a wellorder on our mice is exactly the comparison lemma, but the important thing is that we can naturally compare our mice more so than the comparison lemma itself.

This also motivates why we must consider mice which are models of only very weak theories: If we are forced to cut down $N$ in the comparison with a mouse $M$ then we must be very careful to not throw away too much, otherwise we might end up with a mouse which is actually $<M$! So we only throw away exactly as much as we have to and this might lead to some $\bar N$ along the way to $N'$ which is not nice, e.g. does not satisfy $\Sigma_1$-replacement. This can happen even if $M, N$ are very nice, so there is no way to avoid this!

Dodd-Jensen mice also stop working at some point and have to be replaced by more and more complicated mice. While Dodd-Jensen mice can be compared using linear iteration, at some point the information we put on mice becomes so dense that iterations along trees become necessary. (It is not so that inner model theorists are merely not clever enough to produce a linear comparison lemma at that level, but there are robust arguments that linear iterations cannot work anymore beyond some point)

So how do we know that we found the right measuring stick? First one might wonder whether we left any gaps in this last step from ${L_\alpha}'s$ to Dodd-Jensen mice. This is an inherently vague worry, yet Jensen's covering Lemma deeply justifies that we made a seamless transition.

How do we know that we found the right measuring stick even in principle? This can only be answered metamathematically. On the one side, the mathematical usefulness of our stick is strong evidence that it is the right tool. Using inner model theory, the exact consistency strength (in the proper sense, not to be confused with the less rigorous notion of "strength" here) of countless natural theories has been computed, e.g. $\mathrm{ZF}+\mathrm{AD}$ or $\mathrm{ZFC}+\neg\mathrm{SCH}$, etc, with the help of inner model theory. On the other hand, we can sometimes do the physicists thing and verify predictions that come out of inner model theory. For example, the least mouse which is a model of $\mathrm{ZC}^-$ also satisfies $\mathrm{ZFC}^-$ (i.e. $\mathrm{ZFC}$-replacement-powerset and $\mathrm{ZFC}$-powerset resp.). This predicts that these two theories are really equiconsistent! It is not obvious (to me) that this should hold, but it really does.

To answer your first question, inner model theory, despite the name, is not so much the theory of inner models, but rather the theory of mice. Sometimes, this leads to beautiful proper class inner models, but usually there is no good way of describing them "directly" (while $L[U]$ can be described directly, this should be thought of as an accident! Higher up, this is not true anymore. There is no good way to describe $M_1$ without talking about mice.)