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 , 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 and ;
- 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 there exists with and . This doesn’t always hold, but to explain when it *does* hold we need to define what is. We say that (zero sharp) exists if one (any) of the following statements hold.

- There exists a non-trivial elementary embedding ;
- There exists a proper class of indiscernibles for L;
- There exists a structure such that
- is amenable;
- ;
- is a normal measure on ;
- is the largest cardinal;
- .

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

Theorem.exists iffcoveringfails for L.

So as long as we’re below 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 . 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 and , 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 (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 is a K-successor cardinal, . This in particular implies that given any V-singular cardinal , .

If that’s not good enough, we can generalise the notion even further – this time to the core model below (zero pistol), which is the sharp of a strong cardinal, defined analogously to . 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 (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 , the sharp of a Woodin cardinal – this core model is also sometimes written as . 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 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 , the sharp of infinitely many Woodin cardinals – this is achieved using the *core model induction* and it has the same properties as .