An _inner model_ is a transitive class model of ZF(C). The first nontrivial inner model was Gödel's constructible universe L, which showed that the axiom of choice and the generalised continuum hypothesis were consistent relative to the axioms of Zermelo–Fraenkel set theory ZF.

However, only weak large cardinal properties survive in L. The principal goal of **inner model theory** is to define a _core model_ K in which large cardinals of V retain their status in K. The core model should be like L, in that its construction should be canonical and accomplished "from below" via definability. It should also be close to V, meaning that we require some form of covering lemma.