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.