Accepted for publication in the Journal of Symbolic Logic.

DOI: 10.1017/jsl.2021.61. PDF. arXiv.
Bibtex.

We analyze the hereditarily ordinal definable sets $\operatorname{HOD}$ in $M_n(x,g)$ for a Turing cone of reals $x$, where $M_n(x)$ is the canonical inner model with $n$ Woodin cardinals build over $x$ and $g$ is generic over $M_n(x)$ for the Lévy collapse up to its bottom inaccessible limit of inaccessible cardinals. We prove that assuming $\boldsymbol\Pi^1_{n+2}$-determinacy, for a Turing cone of reals $x$, $\operatorname{HOD}^{M_n(x,g)} = M_n(\mathcal{M}_{\infty} | \delta_\infty, \Lambda),$ where $\mathcal{M}_\infty$ is a direct limit of iterates of a certain initial segment of $M_{n+1}$, $\delta_\infty$ is the unique Woodin cardinal in $\mathcal{M}_\infty$, and $\Lambda$ is a partial iteration strategy for $\mathcal{M}_{\infty}$. It will also be shown that under the same hypothesis $\operatorname{HOD}^{M_n(x,g)}$ satisfies $\operatorname{GCH}$.