Ordinal definability in $L[\mathbb{E}]$

Abstract

Let $M$ be a tame mouse modelling ZFC. We show that $M$ satisfies "$V={\mathrm{HOD}}_x$ for some real $x$", and that the restriction $\mathbb{E}\upharpoonright [{\omega }_1^M,{\mathrm{OR}}^M)$ of the extender sequence ${\mathbb{E}}^M$ of $M$ to indices above ${\omega }_1^M$ is definable without parameters over the universe of $M$. We show that $M$ has universe ${\mathrm{HOD}}^M[X]$, where $X=M|{\omega }_1^M$ is the initial segment of $M$ of height ${\omega }_1^M$ (including ${\mathbb{E}}^M\upharpoonright {\omega }_1^M$), and that ${\mathrm{HOD}}^M$ is the universe of a premouse over some $t\subseteq {\omega }_2^M$. We also show that $M$ has no proper grounds via strategically $\sigma$-closed forcings. We then extend some of these results partially to non-tame mice, including a proof that many natural $\phi$-minimal mice model "$V=\mathrm{HOD}$", assuming a certain fine structural hypothesis whose proof has almost been given elsewhere.

48 pages. Added hypotheses to Thms 1.4 and 1.6, to bridge minor gaps in their former "proofs". Appeal to [6, Thm 0.2] (in paper's references) for Thm 4.2 clarified. Last part of proof of Thm 4.7 clarified. Added Lem 8.14 and strengthened Lem 8.13, to establish what was claimed to be an "immediate consequence" of STH in previous version. Other minor corrections and improvements in exposition

References in corpus (2)

• Iterability for (transfinite) stacks
• Fine structure from normal iterability

Cited by in corpus (2)

• Fine structure from normal iterability
• Varsovian models II