Class forcings and elementary embeddings In the Hamkins-Kirmayer-Perlmutter paper "Generalizations Of The Kunen Inconsistency", they prove the following theorem:
"Theorem 7:  In any set forcing extension $V[G]$, there is no nontrivial elementary embedding $j:$$V$$\rightarrow$$V[G]$ [$V$$\vDash$$ZFC$--my comment].
They note:
"Attribution for this... theorem is not clear to us.  It may have been known to Woodin, and Matt Foreman mentioned to the first author that he had discussed a version of it with Mack Stanley and Sy Friedman in the 1980's, but their proof was different from ours here and their result unpublished$.^{2}$"
Here is their footnote [2]:
"Part of their focus was reportedly on the extent to which the result generalized to class forcing.  For example, they considered the case of class forcing extensions by amenable class forcings.  Foreman mentioned that  Woodin has an example of forcing using a class version of non-stationary tower forcing where $j:$$V$$\rightarrow$$V[G]$, but $V[G]$ does not have $ZFC$ for for the predicate $V$...."
[Edit]  Apparently, one has that when replaces 'set forcing' with 'class forcing' in Theorem 7, one can have a nontrivial elementary embedding $j:$$V$$\rightarrow$$V[G]$.  This seems to contradict Kunen's inconsistency, but the comments made seem to say no.  Why is this?  
 A: Suppose we have an elementary embedding $j: V\rightarrow V[G]$; why should we expect $ran(j)\subset V$? This would only need to be true if $V$ were definable in $V[G]$. Now, by a theorem of Laver (and independently Woodin, I think) $V$ is indeed definable in any set-generic extension, but this fails dramatically for class-generic extensions; see Definability of ground model. And indeed, I believe Woodin’s elementary embedding sends some things in $V$ outside of $V$. EDIT: this belief is correct, see Joel's comment below.

By the way, note that even if we knew $ran(j)\subset V$, there is in principal a second obstacle which could arise: restricting the codomain can kill elementarity! Exercise: we can construct structures $\mathcal{A}\subset\mathcal{B}$ in a language with one binary function symbol $f$ and an elementary embedding $j: \mathcal{A}\rightarrow\mathcal{B}$ with $ran(j)\subset\mathcal{A}$, such that for some $a\in\mathcal{A}$ we have:


*

*$\mathcal{A}\models\neg\exists y\forall z f(y, z)=a$,

*$\mathcal{B}\models\neg\exists y\forall z f(y, z)=j(a),$ but

*there is some $b\in\mathcal{A}$ such that for all $c\in\mathcal{A}$, $f(b, c)=j(a)$.
(Note that we will necessarily have $\mathcal{A}\not\prec\mathcal{B}$.) This obstacle is the reason Theorem 7 of Hamkins-Kirmayer-Perlmutter isn't a one-line corollary of Laver's theorem.
