What is the "strongest" core model to this day? In particular, how far are we from a core model for supercompact cardinals? There are rumors of some notes from a workshop in 2004: https://www.math.cmu.edu/~eschimme/AIM/LongDescription.html
But I couldn't find any more details with respect to a new core model.
Also, could someone recommend the clearest and most rigorous exposition of the "strongest" core model so far?
${}$Hi Ioanna,
I.
The answer probably depends on how we define core model. At the level of "there are no Woodin cardinals in any inner model", we can finally show that core models exist, provably in $\mathsf{ZFC}$. The result was known before, of course, but we needed extra assumptions (such as: There is a measurable cardinal $\kappa$) that allowed us to build the model, but only locally (say, in $V_\kappa$). That $\mathsf{ZFC}$ suffices has recently been established by Jensen and Steel, in $K$ without the measurable.
This paper also contains an axiomatization of what we mean by a core model (see their Theorem 1.1).
Past one Woodin cardinal, the theory turns complicated for a variety of reasons, the first of which being that iterability is no longer an absolute notion, so additional assumptions on the universe of sets are needed to establish the appropriate results. The idea is simple, but making it rigorous takes work: We can relativize the construction of $K$ to $K_x$ where, instead of considering premice, we look at $x$-premice, that are just like premice but have $x$ as an additional object "added at the bottom". If $x$ is itself a mouse, what we are doing is building mice that extend $x$, but now we only look at iterations that do not require us going back to the extenders of $x$. This way, we can then build appropriate versions of the core model for any finite number of Woodin cardinals, inductively (we start with $x$ having one Woodin cardinal, and build $K$ over $x$, establish somehow that weak covering is violated so the construction actually reaches a Woodin cardinal, so now we have models with two Woodin cardinals, we can use these models $y$ to build $K$ on top, etc.
Making this precise requires that we be able to "patch" together local structures into global ones, which is typically why we need additional assumptions (such as, $V$ is closed under sharps). The precise nature of these assumptions obviously ends up depending on the setting we work with, but we can axiomatize the whole process. This leads to the core model induction which, finally, we can truly describe as an induction, The specific requirement on $V$ then becomes closure under appropriate "mice operators". An excellent description of this approach, and how far it can get, can be seen in the Schindler-Steel monograph The core model induction.
As explained in the book, how far the induction can reach (that is, how strong can we obtain a core model) is intimately tied up with how much determinacy we can prove (and so, measuring the strength of the core models becomes a problem of the strength of determinacy assumptions). This is because to obtain closure under the appropriate operators requires that we prove different instances of "mice capturing", for which determinacy appears essential. Nowadays, we understand that the relevant descriptive set theory and inner model theory are so intimately related that we talk of Descriptive inner model theory.
We can reach far beyond what is described in the Schindler-Steel book, and the theory keeps advancing rapidly, so a precise statement of how far we are at is hard to locate. The theory has been mainly developed by Sargsyan, and strongest written results I am aware of are due to him and Trang, see The largest Suslin axiom and Sargsyan's list of publications on his website.
Part of what Sargsyan has done is to identify what seems to be the right hierarchy of mice within models of determinacy. From earlier work of Woodin we knew that the relevant $\mathsf{ZFC}$ models to study were the relativizations of the class $\mathsf{HOD}$ to the models of determinacy. The appropriate hierarchy of hybrid mice we now call hod mice. Their "hybrid" nature means that they are not pure mice, but add fragments of the relevant iteration strategies to them. Their strength is then measured via the Solovay sequence of the determinacy models we consider. In turn, we use these mice to prove determinacy of stronger models, so the process is truly inductive. Here, the Solovay sequence is the sequence of "local" $\theta$ ordinals: $\theta_0$ is the smallest non-zero ordinal not the surjective image of $\mathbb R$ via an ordinal definable map. We can then define $\theta_1$ as the smallest non-zero ordinal not the surjective image of $\mathbb R$ via maps that are ordinal definable in $A$, where $A$ is any set of reals of Wadge degree $\theta_0$, etc. The hierarchy stops once we reach (true) $\Theta$, the first non-zero ordinal not the surjective image of $\mathbb R$.
The expectation Sargsyan has is that the Solovay hierarchy should at least reach as far as the large cardinal hierarchy. The core models we build this way would have strength measured in terms of the Solovay sequence, and to identify their strength in traditional large cardinal terms would then require a further translation. This is now described in some detail in various places, see for instance his paper on The core model induction beyond $L(\Bbb R)$ in the arXiv. As you see there, the final translation (in this case, from "there is an inner model $M$ containing $\mathbb R$ and satisfying $\mathsf{AD}_{\mathbb R}+\Theta$ is regular" to something past "there is an inner model of $\mathsf{ZFC}$ where there is a proper class of Woodin cardinals and a proper class of strong cardinals") requires a non-trivial amount of work. It usually builds on results of Neeman (on models with a Woodin limit of Woodin cardinals) and Jensen-Schimmerling-Schindler-Steel on Stacking mice.
From the above, you probably see that we can currently produce core models essentially in the neighborhood of "There is a Woodin limit of Woodin cardinals". There are natural benchmarks to go from here, say: Models with a measurable Woodin cardinal, or with a subcompact cardinal. This is still significantly below supercompact cardinals, and there are many technical obstacles to overcome before reaching that far.
II.
Independently of the line of developments outlined above, Woodin has a program that attempts to identify what should be the ultimate core model, for all large cardinal assumptions. It is this program and related results that are described on his papers on Ultimate $L$ and what he calls suitable extender models (I, II), particularly see his Midrasha lectures. Woodin's high level program has two parts: First, we identify the coarse features of appropriate models of strong large cardinals, in particular, we identify what their extender sequences should look like, and what the appropriate comparison process and iterability assumptions should be. (This is akin to the isolation of Martin-Steel models for Woodin cardinals, that predated the development of their fine-structure by Mitchell-Steel). This part has had reasonable success. Of course, we do not have proofs yet of the appropriate iterability assumptions, but have instead identified what seem to be the relevant conjectures to pursue in this area.
The success of the second part seems to be still far away (even assuming the truth of the relevant conjectures). Woodin has worked on the fine structure of suitable extender models, but I do not know the current state of his results.
I think the short answer is that we are still a long way from a full core model for a supercompact cardinal.
We have core models (in the sense of Steel's `Core Model Iterability Problem' Lecture Notes in Logic No. 8) for finitely many Woodin cardinals, or perhaps infinitely many such, written out in detail, using the Mitchell Steel fine structural approach. This used an auxiliary assumption of a measurable cardinal $\Omega$ to build the core model up to that level.
Jensen and Steel have in one direction the best current fully written out result proving (in ZFC alone) that if there is no proper class inner model for a Woodin then there is a model K, the core model, which is absolutely definable, invariant under set forcings and enjoys a weak covering lemma. There is a nice section there on the history of this to date. (`K without the measurable' Jensen, Steel, JSL Sep. 2013.)
The construction of further core models is currently stuck by the difficulties of showing sufficient iterability of the models needed to build such. The best results to-date are by Itay Neeman showing that iterability does hold up to a point just beyond at the level of a Woodin which is a limit of cardinals strong up to that Woodin. These are fine structural inner models containing say, a Woodin limit of Woodins (Neeman APAL 2002). And we have some idea of what the models would look like some distance beyond this, if this hurdle could be overcome.
Woodin has an ambitious plan to build inner models for supercompacts using so-called long extenders. But work on this, and in particular on their fine structure, I think is fair to say is still a work-in-progress.
The following may not be an answer to your question, but I think it is related. I have taken it from the introduction of a joint work I am doing with James Cummings and Sy Friedman (which has now appeared):
An important development in large cardinal theory is the construction of inner models $M$ all of whose sets are definable from ordinals and which serve as good approximations to the entire universe $V$. The former means that $M$ is contained in $HOD$, the universe of hereditarily ordinal definable sets, and the latter can be interpreted in a number of ways. One such interpretation is that the cardinal structure of $M$ is ``close'' to that of $V$ in the sense that $\alpha^+$ of $M$ equals $\alpha^+$ of $V$ for many cardinals $\alpha.$ This is for example the case if $V$ does not contain $0^{\sharp}$ and $M$ equals $L$, or if $V$ does not contain an inner model with a Woodin cardinal and $M$ is the core model $K$ for a Woodin cardinal.
The following theorem shows that we can't hope to approximate the cardinals of $V$ by those of (inner models of) $HOD$ in general:
Theorem Suppose $GCH$ holds and $\kappa$ is a $\kappa^{+4}-$supercompact cardinal. Then there is a generic extension $V^*$ of $V$ in which $\kappa$ remains inaccessible and for all infinite cardinals $\alpha <\kappa,$ $(\alpha^{+})^{HOD}<\alpha^{+}.$ In particular $W=V_{\kappa}^{V^{*}}$ is a model of $ZFC$ in which for all infinite cardinals $\alpha, (\alpha^{+})^{HOD}<\alpha^{+}.$
