I have seen mentioned that by a result of Laver, the ground model is definable in any set forcing extension (using parameters).
Does the same hold for class forcing? If it does, in order to establish this fact, does one need to assume more properties about the class-forcing notion, apart from the obvious preservation of the ZFC axioms?
References would also be welcome, since my only current source is the (admittedly short) passage on class forcing in Jech's book.
Let me address the two questions that have arisen here.
First, the question is whether there a significant collection of class forcing notions for which the Laver theorem continues to hold? The answer is yes.
Theorem. (Hamkins) $\ $ If an extension $V\subset W$ of models of ZFC exhibits the $\delta$-approximation and cover properties, then $V$ is definable in $W$ using parameters in $V$.
Unfortunately, this particular theorem is not published explicitly as such. Nevertheless, the proof that Laver gives of the ground model definability theorem in his paper Certain very large cardinals are not created in small forcing extensions (prepublication version), a proof he credits to me, actually achieves this stronger version of the theorem. (The terminology is defined in my paper Extensions with the approximation and cover properties have no new large cardinals, as well as in Laver's paper.)
The way it happened was this. Laver had proved his remarkable ground model definability theorem in the case of set forcing and had contacted me about it---without sending me his proof, which I have never seen---when he noticed, he said, a resemblance in his argument to an argument that Woodin and I had used in our paper Small forcing creates no new strong or Woodin cardinals, a method that was also the basis for my paper on the approximation and cover properties linked above. I was immediately excited about Laver's idea, and in reply I sent him a proof of the stronger theorem above. He responded that this was clearly the right argument even in the case of set forcing, and he proceeded to use my proof in his paper, graciously crediting it to me. Meanwhile, Woodin had independently concluded the set-forcing case implicitly in some of his work. Fascinated with the ground model definability result, Jonas Reitz and I shortly formulated the Ground Axiom, on which Jonas wrote his dissertation, and these ideas formed the basis of our subsequent joint work with Gunter Fuchs on set-theoretic geology.
The key point here in relation to the question is that the collection of class forcing notions that do exhibit the $\delta$-approximation and cover properties is rather extensive and includes many of the standard class forcing notions, such as the forcing of the GCH, progressively closed Easton iterations, the usual forcing of V=HOD, the Laver preparation and many others. Any forcing notion that can be factored as forcing of size $\delta$ followed by $\leq\delta$-closed forcing has the $\delta^+$-approximation and cover properties. So for example, adding a Cohen real and then doing countably closed forcing will have the $\omega_1$-approximation and cover property.
The second question is, does Laver's ground model definability theorem hold for all class forcing notions?
For this, as mentioned in the comments, the answer is no. Consider the following argument, a version of which I recently heard from Carolin Antos-Kuby, a student of Sy Friedman, during a recent trip to Vienna, and this may be due to Sy. Let $\mathbb{P}$ be the Easton support class product forcing over V that adds a Cohen subset to every regular cardinal, and let $V[G][H]$ be $V$-generic for $\mathbb{P}\times\mathbb{P}$, which is actually forcing equivalent to $\mathbb{P}$, since adding two Cohen sets is the same as adding one. Consider the model $V[G]$, which is a ground model of $V[G][H]$, but which we will show cannot be definable there by parameters. Suppose $A$ is any set in $V[G][H]$ and suppose toward contradiction that $\varphi(x,A)$ defines the relation $x\in V[G]$ in $V[G][H]$, forced by some condition $p$. Far above $A$ and the support of $p$, however, we may apply an automorphism $\pi$ of the product forcing $\mathbb{P}\times\mathbb{P}$ that swaps a factor of $G$ on some large coordinate with the corresponding factor of $H$, but fixes the lower part of the forcing, and hence fixes the name of $A$ and the condition $p$. It follows that the definition $\varphi(x,A)$ should also define $V[\pi(G)]$, which by design is not the same as $V[G]$, a contradiction. So there can be no such definition.
