Is it consistent with ZF that the satisfaction relation of $L(P(Ord))$ is $Δ^V_2$ definable? More generally, is it consistent with ZF that there is a $Δ^V_2$ formula (taking $α$ as a parameter) that for every ordinal $α$ gives the satisfaction relation for $L(P^α(Ord))$? $P^α$ is the $α$th iteration of the power set, so $P(Ord)$ is the class of all sets of ordinals, $P(P(Ord))$ the class of all sets of sets of ordinals and so on.
Preferably, the model would satisfy DC and be expandable (by adding a generic well-ordering of $V$) to a model of ZFC. Also, for ZFC, from an inaccessible cardinal, I think we can arrange the weakening that uses $L(Ord^α)$ instead of $L(P^α(Ord))$: Start with $V_κ$ for an inaccessible $κ$, perhaps preparing it; add satisfaction relation for $(L(Ord^ω))^{V_κ}$ by countably closed forcing, and then repeat with other satisfaction relations and higher degrees of forcing closure.
Note that non-OD sets in $P(Ord)$ might camouflage the HOD, so a positive answer to the question might not imply that not much is definable in HOD.
Zero sharp leads to the satisfaction relation for $L$ (despite $L$ being a proper class), and under large cardinal axioms we similarly get the sharp for the Chang model $L(Ord^ω)$. With the axiom of choice, every set is constructible from a set of ordinals. Without choice, however, perhaps in natural models sets of ordinals have little power, analogously to how under AD every subset of $ω_1$ is constructible from a real. Thus, perhaps some set of reals acts as the sharp for $L(P(Ord))$ such that iterating it gives the relevant satisfaction relation, and similarly a set of sets of reals might be the sharp of $L(P(P(Ord)))$, and so on.
Models in which choice fails might seem tangential to the theory of the true $V$. However, the axiom of determinacy gives a good theory of the continuum and natural sets of reals; and the hope is to obtain analogous statements for higher types, and get a good theory for natural sets of natural sets of reals, and so on. Perhaps we get a canonical universe of hereditarily natural sets $W$ such that $V$ or a model elementarily embeddable into $V$ is a canonical class generic extension of $W$ obtained by adding a generic well-ordering (or under generic multiverse pluralism, with multiple choices for the extension). See my FOM posting The universe of hereditarily natural sets. The above is a possible vision for how descriptive complexity in $W$ will work.
