Candidate Inner Models for HOD Under Determinacy

Definitions and mathematical statement

Assume the source's hypothesis of $\Delta^1_3$-determinacy. Determinacy means that one of the two players has a winning strategy in each relevant infinite game of perfect information; the supplied record does not specify the parameter convention for the pointclass $\Delta^1_3$.

Let $N$ be the iterate arising from the report's directed system of suitable premice, let $\delta^N$ be its designated Woodin cardinal, and let $\pi^*$ be the induced cofinal map. These descriptions refer to constructions in the cited report: the supplied record does not define suitability, the directed system, the iteration maps, or the domain and codomain of $\pi^*$. Write \[ M=L[N\mid\delta^N,\pi^*], \] where $N\mid\delta^N$ denotes the indicated initial segment of $N$, and the precise construction of $L[N\mid\delta^N,\pi^*]$ remains source-dependent.

For a real $x$, $L[x]$ denotes the constructible universe relative to $x$, and $\operatorname{HOD}^{L[x]}$ denotes the class of sets that $L[x]$ regards as hereditarily ordinal definable. For structures $\mathcal M$ and $\mathcal H$, elementary equivalence in the language $\{\in\}$ means agreement on every first-order sentence $\varphi$ in that language: \[ \mathcal M\models\varphi\quad\Longleftrightarrow\quad\mathcal H\models\varphi. \]

The question is whether, under the stated determinacy hypothesis and with the report's constructions understood, \[ L[N\mid\delta^N,\pi^*]\equiv\operatorname{HOD}^{L[x]} \qquad\text{for a cone of reals }x. \] If "cone" means a Turing cone and the data $N,\delta^N,\pi^*$ are fixed before quantifying over $x$, this target has the explicit quantifier form \[ \exists y\in{\mathbb{R}}\;\forall x\in{\mathbb{R}}\; \left(y\leq_T x\ \Longrightarrow\ M\equiv\operatorname{HOD}^{L[x]}\right), \] where $y\leq_T x$ means that $y$ is Turing computable from $x$. This expansion is conditional: the supplied record does not specify the cone ordering, whether the constructed data depend on $x$, or the language of elementary equivalence. Consequently, the supplied formulation remains a source-dependent question, rather than a fully specified standalone statement.

Short English statement

Under $\Delta^1_3$-determinacy, does the inner model constructed from the report's iterate and cofinal map satisfy exactly the same first-order sentences as $\operatorname{HOD}^{L[x]}$ for all reals $x$ in a cone? The construction and several conventions require clarification from the source.

Sources

• Supplied local UnsolvedMath registry record, permanent ID $30003407$, exact source problem code catalogue entry, titled "Candidate Inner Models for HOD Under Determinacy," in the Oberwolfach Reports Open Problems collection. The record gives proposed year $2017$ and supplies no named proposer.
• Supplied report citation: Set Theory (2018), Oberwolfach Reports, DOI 10.4171/owr/2017/11, pp. 527--589. https://doi.org/10.4171/owr/2017/11. The year in the supplied title differs from the DOI year and the recorded proposed year; this discrepancy is unresolved here.
• Supplied literature source, "Oberwolfach report": https://ems.press/content/serial-article-files/46674.
• Supplied literature source, "Zhu, HOD structure": https://arxiv.org/abs/1711.02007.
• Supplied literature source, "Zhu, higher sharp IV": https://arxiv.org/abs/1706.00660.
• Literature assessment dated exactly 2026-08-21: the supplied curation labels the problem partially solved and states that substantial initial segments of the HOD structure in $L[x]$ are known under $\Delta^1_3$-determinacy, while the displayed elementary-equivalence question for a cone of reals remains unresolved. This is supplied dated curation, not an independently verified literature assessment; the background explicitly requests independent verification of time-sensitive status and cited claims.
• The registry labels the statement corrected_verified and reports that the official report was checked directly and that definitions were restored while retaining the target. These are supplied provenance claims, not verification performed for this draft.