# Definability in HOD

Let $\mathfrak{M}$ be a countable transitive model of set theory, and consider HOD (the hereditarily ordinal definable elements of $\mathfrak{M}$).

Let $x$ be an object $x \in HOD$. So $x$ is hereditarily definable from ordinals.

Can we find a defining formula $\psi(x)$ of $x$ such that $\psi(x)$ contain only quantifiers ranging over the ordinals?

PS: by "ranging over ordinals" I mean a quantifier $Qy$ where either we have the restriction $Qy$($y$ is an ordinal ...) or that $Qy \in \alpha$ where $\alpha$ is an ordinal.

Edit: After Emil's comment, I am going to allow quantification over elements $y$ such that $y \in x$. The reason for this change is that in the application I have in mind we can allow this. And, yes, we can allow also arbitrary bounded quantifiers.

• If this is true for $x$ not an ordinal itself, $\psi$ can only (usefully) access $x$ through subformulas of the form $y\in x$, where $y$ is an ordinal (quantified or parameter). Thus, if $x\ne x'$ are in $\mathrm{HOD}-\mathrm{Ord}$ and $x\cap\mathrm{Ord}=x'\cap\mathrm{Ord}$, they cannot both have a defining formula of this form. – Emil Jeřábek Dec 5 '13 at 14:25
• In the second paragraph you wrote, about an object $x\in HOD$, that "$x$ is hereditarily definable from ordinals in $HOD$." If "in $HOD$" was intended to apply to "definable", then it is wrong; a set in $HOD$ need not be $OD$ in $HOD$. If "in $HOD$" was intended to apply to "ordinals", then it is trivial, as all ordinals are in $HOD$. – Andreas Blass Dec 5 '13 at 14:38
• The correction should also affect the third paragraph. Presumably, the definitions $\psi$ that you want are definitions in the universe, not in $HOD$. – Andreas Blass Dec 5 '13 at 14:44
• The modification only shifts the problem one level down, that is, $x$ and $x'$ are indistinguishable by such a formula if $\forall y\in x\,\exists y'\in x'\,(y\cap\mathrm{Ord}=y'\cap\mathrm{Ord})$ and vice versa. Couldn’t you allow the formula to contain arbitrary bounded quantifiers? – Emil Jeřábek Dec 5 '13 at 14:45

The answer is no, not necessarily. The main reason is that if $\varphi(x,\vec\alpha)$ is a formula all of whose quantifiers range only over ordinals or are bounded, with ordinal parameters $\vec\alpha$, then the truth of $\varphi(x,\vec\alpha)$ is invariant under extensions $V\subset W$ with the same ordinals and no new elements of sets in $V$, since the interpretation of the meaning of the formula does not change. In particular, the interpretation of $\varphi$ does not change by forcing.
Consider the following example. Start in $L$, and add a Cohen real $L[c]$, and the force to make that real $c$ definable in a forcing extension $L[c][G]$, by forcing to code its digits into the GCH pattern on the $\aleph_n$'s, for example. So $c$ is in $\text{HOD}^{L[c][G]}$, but by further forcing, we can collapse cardinals to $L[c][G][H]$, where $\text{HOD}=L$ again. Suppose that there were a nice formula $\varphi$ defining $c$ in $L[c][G]$. It follows that $\varphi(c)$ also holds in $L[c][G][H]$. But in this case, there is some condition forcing it, and this condition specifies only finitely much of $c$. Since the forcing overall is weakly homogeneous, we may find an automorphic image $d\in L[c]$ of $c$ that also contains that finite part of $c$, and so $\varphi(d)$ will also hold in $L[c][G][H]$, and therefore also in $L[c][G]$. This contradicts that $c$ was defined by $\varphi$ in $L[c][G]$.
• I was about to write that after a bit more thought, the modification still does not work as it a priori restricts every quantifier to Ord or to $\bigcup\dots\bigcup x$ for a fixed number of $\bigcup$'s, and what one really needs is to be able to quantify over the transitive closure of $x$. However, Joel’s argument applies in this case as well. – Emil Jeřábek Dec 5 '13 at 14:55
• I have a different question, it would be better to ask elsewhere maybe but here it goes: if $x$ is in HOD, then the defining formula for $x$ has quantifiers (bounded or unbounded) supposed to range over the whole universe, in the sense it is not restricted to HOD. If that's the case, then it would solve my problem already. – user38200 Dec 5 '13 at 14:59
• A set $x$ is in HOD when it is ordinal-definable in $V$, the larger ambient universe in which HOD is defined. That is, the definition runs in the larger universe $V$, not inside HOD. There is no expectation that the definition still works inside HOD, and as Andreas mentioned, generally the HOD as computed inside HOD might be strictly smaller than HOD. One can define HOD${}^n$ by iterating the HOD construction $n$ times. – Joel David Hamkins Dec 5 '13 at 15:01