# Second-order ordinal definability

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}$$?

## 1 Answer

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$$.