Second-order ordinal definability

Question

As is familiar, a set $S$ is ordinal definable ($S \in \mathsf{OD}$) just in case there exists a formula $\varphi(x, \vec{z})$ of the first-order language of set theory with parameters $\vec{z} = z_1, \ldots, z_n \in \mathsf{On}$ defining $S$, and $S$ is hereditarily ordinal definable ($S \in \mathsf{HOD}$) just in case $S \in \mathsf{OD}$ and $x \in \mathsf{OD}$ for all $x \in \mathrm{trcl}(S)$.

This notion has a natural second-order analogue: working in $\mathsf{ZFC}^2$ (for these purposes $= \mathsf{MK}$), we can say that $\mathsf{OD}^2$ is the class of all sets definable by a formula $\varphi(x, \vec{z}, \vec{Z})$ of the second-order language of set theory with first-order parameters $\vec{z} = z_1, \ldots, z_n \in \mathsf{On}$ and second-order parameters $\vec{Z} = Z_1, \ldots, Z_n \subseteq \mathsf{On}$, and we can define $\mathsf{HOD}^2 = \{ S \vert S \in \mathsf{OD} \wedge \forall x(x \in \mathrm{trcl}(S) \rightarrow x \in \mathsf{OD}) \}.$

Does anyone know of work on $\mathsf{HOD}^2$? Obviously $\mathsf{HOD}^2 = \mathsf{HOD}$ is consistent by a simple construction from a model of $ZFC + V = \mathsf{HOD}$ of inaccessible height. But what else can we say? Is there an obvious construction of a model of $\mathsf{ZFC}^2 + \mathsf{HOD}^2 \neq \mathsf{HOD}$?

Answer 1

Since you allow arbitrary sets of ordinals in your second-order definitions, all sets will be in $\text{OD}^2$. The reason is that, for any set $x$, we can code $x$ into a set of ordinals as follows. Since the axiom of choice is assumed, there is a bijection $f$ from some ordinal $\xi$ onto the transitive closure $t$ of $\{x\}$. Use $f$ to transport the membership relation on $t$ to a binary relation $E$ on $\xi$. Then use your favorite definable pairing function on ordinals to code $E$ as a set $Z$ of ordinals. From $Z$, you can define $E$, and then define $t$ and the membership relation on it (by Mostowski collapsing $E$), and then define $x$.