Let $P$ be the Levy-collapse of the ordinals, so $P$ is a class forcing notion that makes every ordinal countable. 


Note that since $P$ is weakly homogeneous, for any formula $\phi(\overline{a})$ with parameters from $\mathbf{V}$, $P$ decides $\phi(\hat{\overline{a}})$. Hence it makes sense to ask whether $(HC, \in)$ is an elementary substructure of $(\mathbf{V}[G], \in)$ for some or any $P$-generic extension $\mathbf{V}[G]$.


Consider the axiom schema $\Phi$ that asserts that $(HC, \in)$ is elementary in $(\mathbf{V}[G], \in)$. 


**Question:** Is $\Phi$ consistent relative to large cardinals, and if so, what is its strength? (Or at least get an upper bound)


As an example, $\Phi$ implies that $\omega\_1$ is inaccessible to the reals. To see this, fix a real number $x$; then $\mathbf{L}[x]$ satisfies the powerset axiom, so $HC \models `` \mathbf{L}[x] \mbox{ satisfies the powerset axiom}"$, so $\mathbf{L}\_{\omega\_1}[x]$ satisfies the powerset axiom.



Consistency Strength of "HC is elementary in V[G]"
$\newcommand\HC{\text{HC}}$Allow me to denote your theory $\Phi$ by "$\HC\prec V[G]$". As you mention, this is not a single statement, 
since we have no truth predicate able to express truth in the
extension $V[G]$, but rather it is expressed as a scheme, asserting of each formula $\varphi$ with parameters
$z\in\HC$ that $\HC\models\varphi[z]$ if and only if
$\Vdash\varphi(\check z)$, where the forcing relation is over the
Levy collapse of all ordinals.


**Theorem.** The following theories are equiconsistent:


1. ZFC plus your theory, $\HC\prec V[G]$, expressed as a scheme.
2. ZFC plus the axiom scheme [Ord is
Mahlo](http://cantorsattic.info/ORD_is_Mahlo), which asserts that every definable (from
parameters) closed unbounded class $C$ of ordinals contains a
regular cardinal.
3. ZFC plus the assertion scheme that $\kappa$ is an [inaccessible reflecting cardinal](http://cantorsattic.info/Reflecting#Inaccessible_reflecting_cardinal). That is, $V\_\kappa\prec V+\kappa$ is inaccessible, expressed as a
scheme.


**Proof.** The equiconsistent of 2 and 3 is explained on the
Cantor's attic page for Ord is Mahlo, to which I linked.


If your axiom holds, then we have $\HC\prec V[G]$. If
$\kappa=\omega\_1^V$, it follows easily that $L\_\kappa\prec L$,
since $L\_\kappa=L^{\HC}$ and $L=L^{V[G]}$. And since also $\kappa$ is
inaccessible in $L$ as you observed, this gives us a model of
statement 3.


Conversely, if statement $3$ holds, then consider the Levy
collapse $V[G]$ of all ordinals. Let $g=G\upharpoonright\kappa$, so that $V[g]$ is the usual Levy collapse of $\kappa$, and $\HC^{V[g]}=V\_\kappa[g]$.
Since $V\_\kappa\prec V$, it is not difficult to see that
$V\_\kappa[g]\prec V[G]$, as follows. If
$V\_\kappa[g]\models\varphi[x]$, then by taking names, we get that
some $p\in g$ forces $\varphi(\dot x)$ in $V\_\kappa$, and so $p$
forces $\varphi(\dot x)$ in $V$, and so $V[G]\models\varphi[x]$. So
$\HC^{V[g]}\prec V[G]$ holds, verifying your theory in $V[g]$.
**QED**


In particular, the axiom is stronger than just an inaccessible cardinal. For example, you could have also continued your observation about inaccessibility to reals to notice that $\omega\_1$ must be a limit of inaccessible cardinals in $L$, since there can be no bound below $\omega\_1$, as that bound would not work in $L^{V[G]}$. Similarly, it must be $\alpha$-inaccessible for every countable $\alpha$, and $\alpha$-hyperinaccessible and so on. Ultimately, of course, you get that $\kappa$ is an inaccessible fully reflecting cardinal in $L$, as I argued.


The axiom Ord is Mahlo is stronger than inaccessible and
$\alpha$-inaccessible and hyperinaccessible and various strong
hyper-degrees of inaccessibility, but strictly weaker than the
existence of a Mahlo cardinal.


