$$The axiom $V=\text{HOD}$, introduced by Gödel, asserts that every set is ordinal definable. This axiom has a subtler foundational aspect than might at first be expected. The reason is that the general concept of “object $x$ is definable using parameter $p$” is not in general first-order expressible in set theory; it is of course a second-order property, which makes sense only relative to a truth predicate, and by Tarski’s theorem, we can have no first-order definable truth predicate. Thus, the phrase “definable using ordinal parameters” is not directly meaningful in the first-order language of set theory without further qualification or explanation. Fortunately, however, it is a remarkable fact that when we allow definitions to use arbitrary ordinal parameters, as we do with $\text{HOD}$, then we can in fact make such qualifications in such a way that the axiom becomes first-order expressible in set theory. Specifically, we say officially that $V=\text{HOD}$ holds, if for every set $x$, there is an ordinal $\theta$ with $x\in V_{\theta }$, for which which $x$ is definable by some formula $\psi (x)$ in the structure $⟨V_{\theta },\in ⟩$ using ordinal parameters. Since $V_{\theta }$ is a set, we may freely make reference to first-order truth in $V_{\theta }$ without requiring any truth predicate in $V$. Certainly any such $x$ as this is also ordinal-definable in $V$, since we may use $\theta$ and the Gödel-code of $\psi$ also as parameters, and note that $x$ is the unique object such that it is in $V_{\theta }$ and satisfies $\psi$ in $V_{\theta }$. (Note that inside an $\omega$-nonstandard model of set theory, we may really need to use $\psi$ as a parameter, since it may be nonstandard, and $x$ may not be definable in $V_{\theta }$ using a meta-theoretically standard natural number; but fortunately, the Gödel code of a formula is an integer, which is still an ordinal, and this issue is the key to the issue.) Conversely, if $x$ is definable in $V$ using formula $\phi (x,\overrightarrow{\alpha })$ with ordinal parameters $\overrightarrow{\alpha }$, then it follows by the reflection theorem that $x$ is defined by $\phi (x,\overrightarrow{\alpha })$ inside some $V_{\theta }$. So this formulation of $V=HOD$ is expressible and exactly captures the desired second-order property that every set is ordinal-definable.

Consider next the axiom $V=\text{HOD}(b)$, asserting that every set is definable from ordinal parameters and parameter $b$. Officially, as before, $V=\text{HOD}(b)$ asserts that for every $x$, there is an ordinal $\theta$, formula $\psi$ and ordinals $\overrightarrow{\alpha }<\theta$, such that $x$ is the unique object in $V_{\theta }$ for which $⟨V_{\theta },\in ⟩\models \psi (x,\overrightarrow{\alpha },b)$, and the reflection argument shows again that this way of defining the axiom exactly captures the intended idea.

The axiom I actually want to focus on is $\mathrm{\exists }b(V=\text{HOD}(b))$, asserting that the universe is $\text{HOD}$ of a set. (I assume ZFC in the background theory.) It turns out that this axiom is constant throughout the generic multiverse.

Theorem. The assertion $\mathrm{\exists }b(V=\text{HOD}(b))$ is forcing invariant.

• If it holds in $V$, then it continues to hold in every set forcing extension of $V$.
• If it holds in $V$, then it holds in every ground of $V$.

Thus, the truth of this axiom is invariant throughout the generic multiverse.

Proof. Suppose that $\text{ZFC}+V=\text{HOD}(b)$, and $V[G]$ is a forcing extension of $V$ by generic filter $G\subset \mathbb{P}\in V$. By the ground-model definability theorem, it follows that $V$ is definable in $V[G]$ from parameter $P(\mathbb{P}{)}^V$. Thus, using this parameter, as well as $b$ and additional ordinal parameters, we can define in $V[G]$ any particular object in $V$. Since this includes all the $\mathbb{P}$-names used to form $V[G]$, it follows that $V[G]=\text{HOD}(b,P(\mathbb{P}{)}^V,G)$, and so $V[G]$ is $\text{HOD}$ of a set, as desired.

Conversely, suppose that $W$ is a ground of $V$, so that $V=W[G]$ for some $W$-generic filter $G\subset \mathbb{P}\in W$, and $V=\text{HOD}(b)$ for some set $b$. Let $\dot{b}$ be a name for which ${\dot{b}}_G=b$. Every object $x\in W$ is definable in $W[G]$ from $b$ and ordinal parameters $\overrightarrow{\alpha }$, so there is some formula $\psi$ for which $x$ is unique such that $\psi (x,b,\overrightarrow{\alpha })$. Thus, there is some condition $p\in \mathbb{P}$ such that $x$ is unique such that $p⊩\psi (\check{x},\dot{b},\check{\overrightarrow{\alpha }})$. If $⟨p_{\beta }\mid \beta <|\mathbb{P}|⟩$ is a fixed enumeration of $\mathbb{P}$ in $W$, then $p=p_{\beta }$ for some ordinal $\beta$, and we may therefore define $x$ in $W$ using ordinal parameters, along with $\dot{b}$ and the fixed enumeration of $\mathbb{P}$. So $W$ thinks the universe is $\text{HOD}$ of a set, as desired.

Since the generic multiverse is obtained by iteratively moving to forcing extensions to grounds, and each such movement preserves the axiom, it follows that $\mathrm{\exists }b(V=\text{HOD}(b))$ is constant throughout the generic multiverse. QED

Theorem. If $V=\text{HOD}(b)$, then there is a forcing extension $V[G]$ in which $V=\text{HOD}$ holds.

Proof. We are working in ZFC. Suppose that $V=\text{HOD}(b)$. We may assume $b$ is a set of ordinals, since such sets can code any given set. Consider the following forcing iteration: first add a Cohen real $c$, and then perform forcing $G$ that codes $c$, $P(\omega {)}^V$ and $b$ into the GCH pattern at uncountable cardinals, and then perform self-encoding forcing $H$ above that coding, coding also $G$ (see my paper on Set-theoretic geology for further details on self-encoding forcing). In the final model $V[c][G][H]$, therefore, the objects $c$, $b$, $P(\omega {)}^V$, $G$ and $H$ are all definable without parameters. Since $V\subset V[c][G][H]$ has a closure point at $\omega$, it satisfies the ${\omega }_1$-approximation and cover properties, and therefore the class $V$ is definable in $V[c][G][H]$ using $P(\omega {)}^V$ as a parameter. Since this parameter is itself definable without parameters, it follows that $V$ is parameter-free definable in $V[c][G][H]$. Since $b$ is also definable there, it follows that every element of $\text{HOD}(b{)}^V=V$ is ordinal-definable in $V[c][G][H]$. And since $c$, $G$ and $H$ are also definable without parameters, we have $V[c][G][H]\models V=\text{HOD}$, as desired. QED

Corollary. The following are equivalent.

1. The universe is $\text{HOD}$ of a set: $\mathrm{\exists }b(V=\text{HOD}(b))$.
2. Somewhere in the generic multiverse, the universe is $\text{HOD}$ of a set.
3. Somewhere in the generic multiverse, the axiom $V=\text{HOD}$ holds.
4. The axiom $V=\text{HOD}$ is forceable.

Proof. This is an immediate consequence of the previous theorems. $1\to 4\to 3\to 2\to 1$. QED

Corollary. The axiom $V=\text{HOD}$, if true, even if true anywhere in the generic multiverse, is a switch.

Proof. A switch is a statement such that both it and its negation are necessarily possible by forcing; that is, in every set forcing extension, one can force the statement to be true and also force it to be false. We can always force $V=\text{HOD}$ to fail, simply by adding a Cohen real. If $V=\text{HOD}$ is true, then by the first theorem, every forcing extension has $V=\text{HOD}(b)$ for some $b$, in which case $V=\text{HOD}$ remains forceable, by the second theorem. QED