Weak Compactness in HOD from Iterated Embeddings

Definitions and mathematical statement

An elementary embedding $j:V\to V$ preserves every first-order formula in the language of set theory: for every such formula $\varphi$ and every finite tuple $\vec a$ from $V$, \[ V\models\varphi(\vec a)\quad\Longleftrightarrow\quad V\models\varphi(j(\vec a)). \] For a nontrivial elementary embedding $e$ that moves an ordinal, its critical point is \[ \operatorname{crit}(e)=\min\{\xi\in\operatorname{Ord}:e(\xi)\ne\xi\}. \] The supplied hypothesis is $(V,j)\models\mathrm{ZF}$, with $j:V\to V$ elementary. The precise axiomatic interpretation of this expanded structure is not specified.

The source prescribes an iteration, indexed by ordinals, by \[ M_0=(V,j),\qquad M_\alpha=(N_\alpha,j_\alpha),\qquad M_{\alpha+1}=(N_\alpha,j_\alpha(j_\alpha)), \] with direct limits at limit ordinals, and writes \[ \lambda=\sup_{n<\omega}\sup\left(\operatorname{crit}(j^n)\right). \] These expressions are retained as supplied. They do not specify the operation $j_\alpha(j_\alpha)$, the transition maps for the direct limits, or the relationship between $j^n$ and the embeddings $j_\alpha$. Consequently, they do not yet determine a self-contained iteration or a unique intended $\lambda$. In particular, interpreting $j^n$ as ordinary composition would make $j^0$ the identity, whose critical point is undefined, and is not adopted here. Nontriviality and the existence of the displayed critical points are required for the expression to make sense but are not explicitly assumed in the record.

Let $\mathrm{HOD}^{V}$ denote the class of hereditarily ordinal-definable sets of the underlying universe $V$: every set in the transitive closure of $\{x\}$ must be definable in $V$ from ordinal parameters. The intended question, conditional on recovering the report's precise iteration and its definition of $\lambda$, is whether every instance satisfying those hypotheses satisfies \[ \mathrm{HOD}^{V}\models\text{``}\lambda\text{ is a weakly compact cardinal.''} \] Here weak compactness means that, internally to $\mathrm{HOD}^{V}$, $\lambda$ is an uncountable strongly inaccessible cardinal and \[ \lambda\longrightarrow(\lambda)^2_2. \] Explicitly, every coloring $c:[\lambda]^2\to\{0,1\}$ belonging to $\mathrm{HOD}^{V}$ has a homogeneous set $H\in\mathrm{HOD}^{V}$ with $H\subseteq\lambda$ and $|H|^{\mathrm{HOD}^{V}}=\lambda$. Strong inaccessibility here means regularity and the strong limit property, with cardinalities and power sets computed internally to $\mathrm{HOD}^{V}$. This explains the proposed conclusion without supplying the missing iteration conventions.

Short English statement

The question asks whether the cardinal arising from the report's iterated elementary-embedding construction must be weakly compact in $\mathrm{HOD}$. The supplied formulas leave essential iteration conventions and the definition of $\lambda$ unresolved, so the intended assertion requires clarification from the cited report. The record labels the problem open; this draft does not independently verify that status.

Sources

• Local UnsolvedMath registry, permanent ID $30004449$, title "Weak Compactness in HOD from Iterated Embeddings," exact source problem code catalogue entry. This draft uses the supplied complete registry record. The recorded proposed year is 2020; no individual proposer is supplied.
• Supplied report citation: Set Theory (2021), Oberwolfach Reports, pp. 797--855, DOI 10.4171/owr/2020/14. Source URL: https://doi.org/10.4171/owr/2020/14. The background describes Oberwolfach Reports as documenting mathematical workshops and their open-problem discussions.
• Supplied literature reference: "Oberwolfach Report 14/2020," https://doi.org/10.4171/owr/2020/14. The literature assessment was checked on 2026-08-22, according to the supplied dated curation, and has not been independently verified for this draft. That assessment labels the problem open, describes the construction as a rank-into-rank iteration limit, and states that known forcing results concerning other large cardinals in HOD do not decide this specific case. The background expressly requests independent verification of time-sensitive status and cited claims.
• The registry assigns statement status corrected_verified and reports that the official Oberwolfach report was checked, the question isolated from surrounding exposition, and notation repaired for self-contained publication. These are supplied verification claims, not verification performed for this draft. The registry's original statement refers only to "the report's iterated elementary-embedding construction."