My question arises from thinking about how we can obtain class forcing extensions from truncations of set forcing extensions in the presence of a (strongly) inaccessible cardinal in the following sense. Let $\kappa$ be an inaccessible cardinal and let $\mathbb P$ be a forcing such that $\mathbb P \subseteq V\_{\kappa}$. Now we can consider $\mathbb P$ simultaneously as a set forcing (in $V$) and as a class forcing over $V\_{\kappa}$. Now let $G$ be a $(V;\mathbb P)$-generic filter. Then we can ask how $V[G]$ and $V\_{\kappa}[G]$ relate to each other, where in this context $V\_{\kappa}[G] := \{ \sigma\_G : \sigma\in V^{\mathbb P}\cap V\_{\kappa} \}$. 


A naive approach would be to conjecture that $V\_{\kappa}[G] = (V\_{\kappa})^{V[G]}$. This is of course not true in general: if $\mathbb P$ is the Levy collapse $\mathrm{Col}(\omega, <\kappa)$, then, e.g., we have $\wp^{V[G]}(\omega) \in (V\_{\kappa})^{V[G]}\setminus V\_\kappa[G]$, the underlying problem being that $(V\_{\kappa})^{V[G]}$ is a model of the power set axiom, whereas $V\_{\kappa}[G]$ is not. 


We can remedy this last problem by considering $H\_{\kappa}$ instead of $V\_\kappa$ in the above argument (which is the same in the ground model); and indeed we get the following 


**Fact:** Let $\kappa$ be inaccessible and $\mathbb P\subseteq H\_{\kappa}^V$ a forcing preserving the regularity of $\kappa$. Let $G$ be a $(V;\mathbb P)$-generic filter. Then $H\_\kappa^V[G] = (H\_\kappa)^{V[G]}$.


*Proof.* The difficult direction is to show that $(H\_\kappa)^{V[G]} \subseteq H\_\kappa^V[G]$. For this let $x\in (H\_\kappa)^{V[G]}$ and assume (inductively) that $x\subseteq H\_\kappa^V[G]$. Then let $\sigma\in V^{\mathbb P}$ be such that $\sigma\_G = x$ and $\mathrm{dom}(\sigma) \subseteq V^{\mathbb P}\cap H\_{\kappa}^V$. In $V[G]$ we define a function $f: x\to \kappa$ by setting
$$ f(y) := \min\{ \alpha < \kappa : \exists\langle \tau, p\rangle\in \sigma\cap V\_{\alpha+1} (p\in G \wedge \tau\_G = y) \} $$  

for any $y\in x$. Now note that $f``x$ is bounded below $\kappa$, since $\kappa$ is regular in $V[G]$ and by assumption there can be no surjection from $x$ onto $\kappa$. Thus take $\alpha < \kappa$ such that $f``x\subseteq \alpha$ and let $\sigma' := \sigma\cap V\_{\alpha}$. Then $\sigma'\_G = \sigma\_G = x$ and $\sigma' \in V^{\mathbb P}\cap H^V\_{\kappa}$ by inaccessibility of $\kappa$ in $V$. Therefore $x\in H\_\kappa^V[G]$. $\Box$ 


This proof depends on the fact that $\mathbb P$ preserves the regularity of $\kappa$, but on the other hand I could not construct a counterexample for a forcing singularizing $\kappa$. This leads me to ask the following


**Question:** Let $\kappa$ be inaccessible. Can there be a forcing $\mathbb P\subseteq H\_{\kappa}^V$ that does not collapse $\kappa$ and such that there is some $(V;\mathbb P)$-generic filter $G$ with $H\_{\kappa}^V[G] \neq (H\_{\kappa})^{V[G]}$ ? 



Class forcing as set forcing followed by truncation
No, there can be no such forcing. The point is that such a forcing should have size $\kappa$ and by my proof given in [Singularizing forcing of "small" cardinality?](https://mathoverflow.net/questions/142086/singularizing-forcing-of-small-cardinality), we have $\Vdash\_{\mathbb{P}} |\kappa|=cf(\kappa)$, so $\mathbb{P}$ can not change the regularity of $\kappa$ as else it collapses $\kappa.$ Now the result follows from your argument.


