Ordinal definability and HOD

In ZF a set $x$ is ordinal definable, written $x\in \mathrm{O}\mathrm{D}$, if there are an ordinal $\theta >0$, finitely many ordinals $a_i<\theta$, and a membership formula code e such that $x\in V_{\theta }$ is the unique element satisfying that formula over $(V_{\theta },\in )$ with those parameters. Here $V_{\theta }$ is precisely the cumulative hierarchy of The cumulative hierarchy, not an arbitrary transitive set closed under some operations. Set satisfaction, with finite tuples as in Finite-tuple satisfaction is absolute, makes OD a single first-order definable class.

Define

$\mathrm{H}\mathrm{O}\mathrm{D}=\{x:\mathrm{TC}(\{x\})\subseteq \mathrm{O}\mathrm{D}\}\mathrm{.}$

The TC convention is the least transitive superset, so it includes x itself when applied to its singleton, by Minimality and closure laws of TC. Thus HOD requires x and every descendant to be OD.

This coded definition agrees, formula by formula, with unique definability in V from finitely many ordinals. If a fixed formula uniquely defines x in V from ordinal parameters, reflect that formula, its uniqueness assertion and their subformulas to a $V_{\theta }$ containing x and the parameters, using Montague–Lévy reflection for a finite formula family. It defines exactly x there. Conversely the particular code e, theta and ordinal tuple witnessing the displayed definition give an ambient unique definition: use the uniformly definable set $V_{\theta }$ and its set satisfaction. The code e is a natural number, hence itself an ordinal parameter. This converse asserts definability for each witness; it does not introduce a truth predicate for V or quantify over arbitrary formulas evaluated in V.