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.
 A: 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]$. 
