# Core models
Core models are inner [models](Model.md "Model") which have certain canonicity properties.
We currently do not have a general abstract definition of a core model, rather there are certain constructions.
Each such construction always requires assuming an *anti-large cardinal assumption*, i.e. that certain large cardinals do not exist.
For example:
- The first core model, [[Dodd-Jensen core model]] ($K^{DJ}$), was introduced in {% cite Dodd1981 %}, assuming there is no inner model with a measurable cardinal.
- The core model built assuming $¬ 0 ^{sword}$ (see [[Zero sword]]) is called *the [[Core model for measures of order 0]]* ($K^{MOZ}$).{% cite Sharpe2011 %}
- [[Mitchell - The core model for sequences of measures. I|Mitchell's core model]] is built under the assumption that there is no inner model with a [[Measurable|measurable]] cardinal $\kappa$ of order $\kappa^{++}$.
- [[Steel - The core model iterability problem| Steel's core model]] is built under the assumption that there is no inner model with a [[Woodin]] cardinal (plus a technical assumption - the existence of a measurable cardinal denoted $\Omega$).
If we state an anti-large cardinal assumption, we refer to the corresponding construction as $K$.
*The* core model is $K^{V}$. *A* core model is a model of the form $K^{M}$ for some transitive class model of ZFC.
Luckily, the definitions form a hierarchy - the definition given a certain anti-large cardinal hypothesis coincides with the definitions given higher anti-large cardinal hypotheses.
So for example, if $\neg 0^{sword}$ holds, then Steel's definition will give Jensen's $K^{MOZ}$.
(See [[Schimmerling - A core model toolbox and guide]])
## Properties expected of core models
- *Fine structure* with the consequence, for example, that GCH and combinatorial principles such as ◇ and $\square$ hold in $K$.
- *Universality* with the consequence, for example, that the existence of certain extender models is absolute to $K$.
- *Maximality* with the consequence, for example, that certain large cardinal properties of $\kappa$ are downward absolute to $K$.
- *Definability* in a way that makes $K$ absolute to set forcing extensions.
- *Covering* with the consequence, for example, that $K$ computes successors of singular cardinals correctly.
(Further informations from {% cite Dodd1981 %})
## From the definition
Definition 6.3:
- $D = \{ \langle \xi, \kappa \rangle \mid \xi \in C_N, N\text{ is a mouse at }$\kappa$, |C_N| = \omega \}$
- $D_\alpha = \{ \langle \xi, \kappa \rangle \mid \xi \in C_N, N \text{ is a mouse at }\kappa, \|C_N\| = \omega, \mathrm{Ord} \cap N < \omega_\alpha \}$
- $K = L[D]$ — **the core model**
- $K_\alpha = |J_\alpha^D|$
Definition 5.4: $N$ is a *mouse* iff $N$ is a critical premouse, $N'$ is
iterable and for each $i \in \mathrm{Ord}$ there is $N_i$, a critical
premouse, such that $(N_i)' = N_i'$ where $\langle N_i',
\pi_{ij}', \kappa_i \rangle$ is the iteration of $N'$, and $n(N_i)= n(N)$.
Definition 5.1: Premouse $N = J_\alpha^U$ is *critical* iff
$\mathcal{P}(\kappa) \cap \Sigma_\omega(N) \not\subseteq N$ and
$N$ is acceptable.
Definition 3.1: For $\kappa < \alpha$, $N = J_\alpha^U$ is a
*premouse* at $\kappa$ iff $N \models
quot;$U$ is a normal measure"
on $\kappa$”}$.
$J_\alpha^A$ is defined using functions rudimentary in $A$
(definitions 1.1, 1.2).
## Properties
The core model $K$ is not absolute, for example: if $0^\sharp$ ([[Zero sharp]]) does not exist, then $K = L$; if $0^\sharp$ exists, but $0^{\sharp\sharp}$
does not, then $K = L[0^\sharp]$.
However, $K^M = M \cap K$ for any inner model $M$.
$K$ will contain “all the sharps” in the universe, but may in general be larger than the model obtained by iterating the $\sharp$ operation
through the ordinals.