What is K?

The core model K is, among other things, great for providing lower bounds for the consistency strength of some interesting theory. For instance, every Jónsson cardinal is Ramsey in K, showing that the two are equiconsistent. Usually there are a lot of different K’s with different properties, sometimes denoted by things like K^{DJ}, K^{Steel} or something along those lines. This is my attempt at (briefly) explaining what K is, and what the differences between the various versions are. Here’s an overview of the various core models I’ll cover:


Intuitively, K is the canonical model of ZFC that looks like L but can accomodate more large cardinals than L. To “look like L” we require at least the following properties of the model:

  • It should be the same in any generic extension of V;
  • It should satisfy things like GCH and combinatorial principles such as \diamondsuit and \square;
  • It should satisfy some kind of covering property.

It’s well-known that L satisfies the first two properties. As for the last one, we say that L satisfies full covering if for every A\subset\text{On} there exists X\in L with A\subseteq X and |A|=|X|. This doesn’t always hold, but to explain when it does hold we need to define what 0^\sharp is. We say that 0^\sharp (zero sharp) exists if one (any) of the following statements hold.

  1. There exists a non-trivial elementary embedding j:L\to L;
  2. There exists a proper class of indiscernibles for L;
  3. There exists a structure \mathcal M=(L_\lambda,\in,\mu) such that
    • \mathcal M is amenable;
    • \mathcal M\models\textsf{ZF}^-;
    • \mathcal M\models\mu is a normal measure on \kappa;
    • \mathcal M\models\kappa is the largest cardinal;
    • \lambda=\kappa^{+\text{Ult}(L_\lambda,\mu)}.

The definition of most interest to us in this post is the third one — such a structure \mathcal M is called an active baby mouse. A key property of the interaction between L and 0^\sharp is then the following.

Theorem. 0^\sharp exists iff covering fails for L.

So as long as we’re below 0^\sharp in the large cardinal hierarchy we get covering, and in this case we simply have K=L. So what about K’s below stronger hypotheses? Dodd and Jensen managed to construct K below a measurable cardinal, also satisfying full covering – this K is sometimes denoted K^{DJ}. This was constructed by “stitching together” various iterable structures called mice.

An important feature these mice have is that they can be compared: given any two mice \mathcal M and \mathcal N, it is possible to iterate each mice using their measure until one of them is an initial segment of the other. Note that these iterations are linear; all we’re doing is applying the top measure on the mice.

The next notable core model is the one built below a gadget called 0^\dagger (zero dagger), which is “the sharp of a measurable cardinal”, by which we mean an active baby mouse which furthermore satisfies that there’s a measurable cardinal below its top measure. This version of K can thus accomodate a measurable cardinal. But this comes at a price: we lose full covering. It’s not all lost however, as we still retain what is known as weak covering: whenever \kappa is a K-successor cardinal, \text{cof}^V(\kappa)=|\kappa|^V. This in particular implies that given any V-singular cardinal \kappa, \kappa^{+K}=\kappa^{+V}.

If that’s not good enough, we can generalise the notion even further – this time to the core model below 0^\mathparagraph (zero pistol), which is the sharp of a strong cardinal, defined analogously to 0^\dagger. The difference is that we’re not only applying a single measure: we now got a sequence of extenders on our models (and thus on K as well). These extenders are non-overlapping, meaning that it’s impossible for an extenders critical point to lie in between another extenders critical point and length. This means that we still have a linear iteration, just applying (possibly) different extenders along the way.

The next core model is the one defined below 0^\bullet\!\!\!\shortmid (zero hand-grenade), which is the sharp of a proper class of strong cardinals. Here we still have extenders, but we move from linear iterations to almost linear iterations (see Definition 2.1 in Schindler (2001)). Lastly we get to the core model below \mathcal M_1^\sharp, the sharp of a Woodin cardinal – this core model is also sometimes written as K^{Steel}. We now go to actual iteration trees, and coupled with still having extenders and only weak covering, we’re a long way from home.

This last core model K^{Steel} is the best core model we can get in ZFC. If we’re willing to assume stronger hypotheses we can get the core model below \mathcal M_\omega^\sharp, the sharp of infinitely many Woodin cardinals – this is achieved using the core model induction and it has the same properties as K^{Steel}.