Consistency Strength of "HC is elementary in V[G]"

Question

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.

Answer 1

$\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, 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. 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.