$\newcommand\gHOD{\text{gHOD}}
\newcommand\HOD{\text{HOD}}
\newcommand\ZFC{\text{ZFC}}
\newcommand\GCH{\text{GCH}}$

I believe that it was Peter Koepke who first proposed that we
should investigate this model, including the question of GCH in
it.

Let me confess at the outset that I am troubled by the very
definition of the model as $\text{HOD}^{V[G]}$. The problem is
that I don't know a sensible way to define $\text{HOD}$ inside
$V[G]$, which, lacking power set, lacks the usual von Neumann
$V_\theta$ hierarchy that is central to the usual definition of
$\text{HOD}$. That is, one usually defines $\text{HOD}$ in a
$\text{ZFC}$ context by saying $x\in\text{HOD}$ if it is ordinal
definable in some structure $\langle V_\theta,{\in}\rangle$. This
is formalizable in set theory, and it works precisely because the
$V_\theta$ sets themselves are ordinal definable. (One cannot say,
naively, that $x$ is ordinal definable just in case there is a
definition of $x$ using ordinal parameters, since this uses a
universal truth predicate, which we cannot have on account of
Tarski's theorem on the non-definability of truth.) I am not aware
of any theory of $\text{HOD}$ that may be undertaken in a
$\text{ZFC}^-$ context. So at the very least, the question needs clarification as to what
$\text{HOD}^{V[G]}$ is supposed to mean.

But let us suppose that this issue can be overcome, and that we
have a definable way to speak of $W=\text{HOD}^{V[G]}$, so that it
is a definable class in $V[G]$ consisting of the ordinal definable
elements there (and certainly, over some models $V$ this
assumption is legitimate). In this case, let me show why $W$ is an
inner model of $\text{ZF}$ contained in $V$. That is, although in
$V[G]$, every set has become countable and so ZF of course fails
there, by moving to the HOD of $V[G]$, you only take the
hereditarily ordinal-definable part of $V[G]$, and I claim this
must in fact be contained in $V$. To see this, note that the
forcing is almost homogeneous, and every condition has an
automorphic image compatible with any other. It follows that any
statement $\varphi(\check x)$ in the forcing language involving
only parameters from the ground model is forced either by every
condition or by none, since the automorphisms fix the names of the
parameters of the statement. It follows that any if all elements
of a hereditarily ordinal definable element of $V[G]$ are in $V$,
then we can determine these elements in $V$ via the forcing
relation. (Note: this argument relies on the forcing lemmas for
the class forcing to make every set countable; but this is OK,
since this forcing is an iteration of set-sized forcing and hence
every set is contained in a set-sized complete subforcing notion.)
Thus, $W\subset V$, and it is a definable transitive class
containing all the ordinals.

To see that $W\models\text{ZF}$, one gets the easier axioms
without much difficulty. Beyond this, we can see that $W\cap
V_\alpha\in W$, by induction on $\alpha$. If true at $\alpha$,
then $W\cap V_\alpha$ is definable in $V[G]$ as the elements of
HOD of rank less than $\alpha$, and so its power set is also
definable in $V[G]$, and is a set there since it is subset of
$V_{\alpha+1}$. If true below a limit $\lambda$, then $W\cap
V_\lambda$ is definable in $V[G]$ as the sets in HOD of rank less
than $\lambda$. Thus, $W$ is almost universal and this gives the
collection axiom, and so $W\models\text{ZF}$.

I don't see yet why we should expect the axiom of choice always to
hold in $W$, and this is related to my issues with the definition
of $W$. Ordinarily, one get AC in HOD by defining in ZFC a
well-ordering of HOD, so that $x\lt y$ just in case $x$ is coded
by a set of ordinals definable in $V_\theta$ for a smaller
$\theta$ than $y$ is, or for the same $\theta$ but with a smaller
definition, or with the same $\theta$ and the same definition, but
with smaller parameters. So, this argument will continue to work
in the context of this question, provided that we define
$\text{HOD}^{V[G]}$ by reference to some kind of ordinal-definable
hierarchy in $V[G]$ inside of which we may run the definitions. So
solving the definition issue mentioned above may also show how to
get AC in $W$. But in general, I am unsure.

Meanwhile, let me mention another approach to a similar model,
about which more progress has been made. Namely, Gunter Fuchs
defined the *generic HOD*, denoted $\text{gHOD}$, and we give some of the basic facts in our paper
Set-theoretic geology.
The generic HOD is the intersection of the HOD's of all the
set-forcing extensions of $V$. $$\text{gHOD}\ \ = \ \
\bigcap_\theta \text{HOD}^{V^{\text{Coll}(\omega,\theta)}}$$
This model is similar to yours, in the sense that we are collapsing more and more sets to be countable, and only taking the sets in the HODs of the models along the way (whereas you take the HOD of the final model at the end, which is not a ZFC model). The nice thing about the generic HOD is that it is an inner model $V$ satisfying $\text{ZFC}$ and containing
all ordinals. One of the theorems of set-theoretic geology is that
every model of set theory arises as the $\text{gHOD}$ of another
model of set theory, a class forcing extension.

**Theorem.** (Fuchs,Hamkins,Reitz Set-theoretic geology) Every model of set theory $V$
is the generic HOD, as well as the HOD, the mantle and the generic
mantle, of another model $V[G]$, obtained by class forcing over
$V$.
$$V=\text{gHOD}^{V[G]}=\text{HOD}^{V[G]}=\text{M}^{V[G]}=\text{gM}^{V[G]}.$$

(The *mantle* of a model of set theory is the intersection of all
the ground models of that model, and the *generic mantle* is the
intersection of the ground models of all the set-forcing
extensions of the model.)

Thus, for the generic HOD version of your question, the answer is
that one cannot make any general assertions about what is true
there, since it could be an arbitrary model of ZFC.

**Update.** Regarding your updated question, yes, in general we should expect $\gHOD$ to be very different from $\HOD^{V[G]}$. For example, for example, if you start with a model having the continuum coding axiom, which asserts that every set of ordinals arises as a block in the $\text{GCH}$ pattern, then $\gHOD=V$, since every set in $V$ continues to be coded high up in the $\GCH$ pattern in any set forcing extenion $V[g]$. Thus, all such sets remain in the $\HOD^{V[g]}$ of any set forcing extension and thus remain in $\gHOD$. But if $V$ as obtained by forcing the continuum coding axiom over some deeper model $V_0$, then the $\HOD^{V[G]}$ will be contained in $V_0$, and hence much smaller than $V=\gHOD$. I guess the homogeneity arguments show that $\HOD^{V[G]}\subset\gHOD$.

(But once again, I don't think we have actually defined $\HOD^{V[G]}$, and so I wouldn't want to state many theorems about it until we have a proper definition.)

4more comments