This short but essential part introduces the core model. Once mice are to hand the definition (14.3) is very simple. Chapter 14 gives the analysis of the Ωκ structure of K and proves that K is a model for GCH and is O-maximal.

Chapter 15 generalises the work of chapter 12 and shows on the one hand that all manner of # iterations can be coded by mice but on the other that before we get very far the situation degenerates into chaos. Mice are, we think, a better way to describe sharps than reals and we single out some “sharplike” mice M#. At this stage M# is only defined if M╞V=K; other cases require the covering lemma and are dealt with in part five.

Chapter 16 introduces a new technique to show that elementary non-trivial embeddings of models M for V=K into themselves imply the existence of M# unless K has its “maximal” form when there is a ρ-model. The ρ-model is a sort of K#, and we have seen in chapter 13 that it behaves like a real mouse (it is assumed that the reader is becoming inured to the absurdity of the terminology).

Chapter 17 covers as many applications as can be covered without the covering lemma. The covering lemma and the singular cardinal hypothesis are the most important applications of K and we reach these in part five. Chapter 17 is not needed for the proof of the covering lemma and could be omitted.