Infinitary generalizations of HOD

Question

Say that a set is ordinal$_{\kappa\lambda}$-definable if it is definable by a formula in the infinitary language $\mathcal{L}_{\kappa\lambda}$ with parameters from $\mathsf{On}$. Let $HOD_{\kappa\lambda}$ be the class of hereditarily ordinal$_{\kappa\lambda}$-definable sets. Definitionally, $HOD_{\omega\omega} = HOD$; by a simple argument given in the citation below, $HOD_{\infty\infty}=V$.

What can we say about $HOD_{\kappa\lambda}$ for other values of $\kappa$ and $\lambda$? Some questions that obviously arise: do we have $\mathsf{Con}(HOD_{\kappa^+\omega}\neq HOD_{\kappa\omega})$ for all $\kappa$? Do we have $\mathsf{Con}(HOD_{\kappa^+\lambda}\neq HOD_{\kappa\lambda})$ for all $\kappa,\lambda$? Do we have $\mathsf{Con}(HOD_{\kappa\lambda^+}\neq HOD_{\kappa\lambda})$ for all $\kappa,\lambda$?

(This question is inspired by the discussion at Gödel's Constructible Universe in Infinitary Logics (A Possible Approach to HOD Problem).)

Answer 1

If the number of parameters is unlimited (i.e. ordinals can be used as literals) (but see the addendum if that is not the case), then $\mathrm{HOD}_{κ,λ} = \mathrm{HOD}_{κ,ω} = \mathrm{HOD}(\mathrm{Ord}^{<κ})$  ($κ$ is regular).
$\mathrm{HOD}(\mathrm{Ord}^{<κ})$ satisfies ZF but (unless $κ=ω$) not necessarily ZFC. It is consistent that for every (infinite) regular $κ$, $\mathrm{HOD}_{κ,ω}$ is a proper subclass of $\mathrm{HOD}_{κ^+,ω}$.

Explanation: $\mathcal{L}_{κ,λ}$ does not add expressiveness over $\mathcal{L}_{κ,ω}$ because $V$ is closed under $<λ$-tuples. Next, an $\mathcal{L}_{κ,ω}$ formula can include $<κ$ parameters/literals, hence the inclusion of $\mathrm{Ord}^{<κ}$ and thus $\mathrm{HOD}(\mathrm{Ord}^{<κ})$. Conversely, because $\mathcal{L}_{κ,ω}$ satisfaction relation for every $V_α$ is first order definable (from $α$) in $V$ (and the formulas are definable from $<κ$ parameters), $\mathrm{HOD}_{κ,ω}$ is included in $\mathrm{HOD}(\mathrm{Ord}^{<κ})$. The consistency results for $\mathrm{HOD}(\mathrm{Ord}^{<κ})$ can be obtained by adding generic subsets to regular cardinals.

Definitional note and caveat: In ZFC, $\mathrm{HOD}$ is essentially defined as $∪_{α<∞} \mathrm{HOD}^{V_α}$, and I assume you mean the analogous definition for $\mathrm{HOD}_{κ,λ}$, which is the only definition that makes sense in ZFC, but a caveat is in order. Using the replacement schema, in every model $M$ of ZFC, every definable set is definable in some $V_α^M$. However, the satisfaction relation for infinitary formulas about $V$ goes beyond the expressiveness of the first order set theory. And to prove the analogous equivalence for $\mathrm{HOD}_{κ,λ}$, we would need to extend the language of set theory and add replacement for appropriate formulas. If we extend the language of set theory but omit the extended replacement, the then (analogously to $\mathrm{HOD}$ in $V_{ω_1}$) it becomes expressible and consistent that our above definition of $\mathrm{HOD}_{κ,λ}$ does not include every set that is hereditarily $\mathcal{L}_{κ,λ}$ definable in $V$ with parameters from $\mathrm{Ord}$ (and we may get various subtleties about definability).

Addendum: If the number of ordinal parameters is below $λ$ (which makes for the best nomenclature of $\mathrm{HOD}_{κ,λ}$), then $\mathrm{HOD}_{κ,λ} = \mathrm{HOD}(H(κ),\mathrm{Ord}^{<λ})$ (note: $H(κ) = \{x: |\operatorname{tc}(x)| < κ \}$) because the infinitary formulas (excluding parameters) can code (and be coded by) elements of $H(κ)$. This does not depend on whether the variable quantification is $\mathcal{L}_{κ,κ}$ or $\mathcal{L}_{κ,ω}$ or somewhere in between. It should be consistent that for all infinite cardinals $κ≥λ,κ'≥λ'$ ($κ$ and $κ'$ are regular), $\mathrm{HOD}_{κ,λ} ⊆ \mathrm{HOD}_{κ',λ'} ⇒ κ≤κ'∧ λ≤λ'$, but I did not verify it.