Why does $\mathsf{HOD}^{V[G]} \subseteq \mathsf{HOD}^V$ hold for weakly homogeneous forcings? A forcing $\mathbb{P}$ is said to be weakly homogeneous if for any $p,q \in \mathbb{P}$ there is an automorphism $\pi$ of $\mathbb{P}$ such that $\pi(p)$ and $q$ are compatible. An important fact about weakly homogeneous forcings $\mathbb{P}$ is that for any formula $\varphi(v_0,\dots,v_{n-1})$ in the forcing language and any $x_0,\dots,x_{n-1} \in V$ we have that every condition of the forcing $\mathbb{P}$ decides $\varphi(\check x_0,\dots, \check x_{n-1})$ in the same way.
I want to prove that for any generic filter $G$ of a weakly homogeneous forcing $\mathbb{P}$, we have $\mathsf{HOD}^{V[G]} \subseteq \mathsf{HOD}^V$.
My idea is to use the fact that forcing preserves the ordinals together with the above mentioned property of weakly homogeneous forcings to show that no new ordinal definable sets are added to $\mathsf{OD}$. Suppose that there is a $\mathbb{P}$-name $\dot x$, a formula $\varphi$ in the forcing language, ordinals $\alpha_0,\dots,\alpha_{n-1}$ and $p \in \mathbb{P}$ such that $p \Vdash \forall y \ y \in \dot x \leftrightarrow \varphi(y,\check \alpha_0,\dots,\check \alpha_{n-1})$. Then, by the above fact, $\mathbb{1_P} \Vdash \forall y \ y \in \dot x \leftrightarrow \varphi(y,\check \alpha_0,\dots,\check \alpha_{n-1})$. Now, if $G$ is $\mathbb{P}$-generic, then $V[G] \vDash \forall y \ y \in \dot x^G \leftrightarrow \varphi(y,\alpha_0,\dots,\alpha_{n-1})$. Since $\varphi(y,\alpha_0,\dots,\alpha_{n-1})$ is by the above fact decided for all conditions of the forcing in the same way, this should somehow show that $\dot x^G$ is already contained in $\mathsf{OD}^V$ and this would imply the claim.
Is this the right approach to do this and how do I close the gaps?
 A: There is a slight caveat here. If $\Bbb P$ is a weakly homogeneous forcing, then $\mathrm{HOD}^{V[G]}\subseteq\mathrm{HOD}^V(\Bbb P)$.
The reason is that we need $\Bbb P$ as a parameter, as the proof goes through the forcing relation of $\Bbb P$, which itself is definable from $\Bbb P$.
Your idea is correct. It is enough to make sure that every set of ordinals in $\mathrm{HOD}^{V[G]}$ is already in $\mathrm{HOD}^V(\Bbb P)$, as these are models of $\sf ZFC$. But now it's easy. If $p\Vdash\varphi(\check\alpha,\check\xi)$, then $1\Vdash\varphi(\check\alpha,\check\xi)$; so the same holds for the negation of $\varphi$. So the set $\{\alpha\mid 1\Vdash\varphi(\check\alpha,\check\xi)\}$ lies in the ground model and it is equal exactly to the set which will be definable in $V[G]$ from $\varphi$ and $\xi$.
Now if $A$ is a set of ordinals which is ordinal-definable in $V[G]$, then taking $\varphi$ to be the definition and $\xi$ the parameter, we get that $A$ lies in $V$ and that it is ordinal-definable there as long as you know the forcing relation of $\Bbb P$.
