Inner model theory without choice

Question

How much of the inner model project can be constructed without assuming the axiom of choice? I.e. which large cardinals provably have canonical inner models not assuming choice?

Answer 1

Addressing the first question: I should argue that Choice comes in almost at the beginning of the inner model project, if we regard proving Covering Lemmata as an integral part of that project: one defines a model under an anti-large cardinal assumption; proves that it is rigid; the Covering Lemma is then proven as holding over that model. One then has the contrapositive that if Covering fails, then so does your anti large cardinal hypothesis, and then we move on to define the ‘next’ inner model that accommodates that large cardinal.

With that in mind, then in ZF alone one can indeed prove that assuming $\neg O^\sharp$ then the (Jensen Strong) Covering Lemma holds over $L$. Dodd & Jensen then defined as the ‘next’ model $K^{DJ}$, the core model ‘below’ a measurable cardinal. The general Covering Lemma $CL$, $\Gamma$ say, then ran:

$\Gamma$: “ Assume $\neg O^{\dagger}$. Then either the Covering Lemma holds over $K^{DJ}$, or it holds over $L[\mu_0]$ where the latter is the least ‘$\rho$-model’, i.e. has a measure $\mu_0$ on some least possible ordinal $\kappa_0$. Or it holds over $L[C]$ where $C$ is a Prikry sequence over $L[\mu_0]$”.

If these three alternatives fail, then we have $O^{\dagger}$ and we look to build the next model, culminating in a model with two measurable cardinals {\em &c.} But $\Gamma$ can only be proven in ZFC. Reason: if one looks at $M = \bigcap_{i< \omega^2}L[\mu_i]$ (where $L[\mu_i]$ is the $i$t’h iterate of the least $\rho$-model, now on $\kappa_i$) this is a ZF model, but the set of Prikry sequences in the model cofinal in the ordinal $\kappa = \kappa_{\omega^2}$ is not wellorderable in $M$. One then ends up with $(\neg \Gamma)^M$.