Can an ultrapower be undone by class forcing?

Suppose I have a transitive model $M$ of ZFC, and - in $M$ - $U$ is a measure on $\kappa$. Then the transitive collapse of the ultrapower of $M$ along $U$ is an inner model, $N\subset M$.

My question is:

Can we ever have $M$ be a class-generic extension of $N$?

Context: The set-forcing version of this question was answered by Douglas Ulrich, using a result of Hamkins-Kirmayer-Perlmutter; and Joel David Hamkins pointed out that the same result holds for many "nice" class forcings. However, the general class-forcing version remains open, and general class forcing is potentially so nasty that I thought this warranted its own question.

• Well, undoing an ultrapower means resurrecting the measurability of a smaller cardinal. If that's even possible, I'd imagine some very very large cardinals are involved; and the measure being something like some type of a huge measure or so. – Asaf Karagila Jan 15 '17 at 6:51
• @AsafKaragila Kunen showed long ago that a non-measurable cardinal can become measurable in a forcing extension, and the consistency strength is just a measurable cardinal. You start with $\kappa$ measurable, and then kill it in a way that it can be resurrected. – Joel David Hamkins Jan 15 '17 at 12:00
• @Joel: Yes, by adding Cohen sets below the measurable, I know (and this way it ends up immune to Cohen sets). But never the less, this is a very different situation from taking an inner model which is an ultrapower by a measure. – Asaf Karagila Jan 15 '17 at 12:10
• I was merely responding to your statement, "...resurrecting the measurability of a smaller cardinal. If that's even possible...". It is possible, by Kunen's theorem. I agree that this does not shed light on Noah's question. – Joel David Hamkins Jan 15 '17 at 12:14

The answer is negative, if one considers parameter-free definable ZFC-preserving class forcing satisfying the forcing theorem, which means that the forcing relation is definable and true statements in the extension are forced.

Theorem. Suppose that $\newcommand\P{\mathbb{P}}\P$ is a ZFC-preserving definable class forcing notion in $M$ that satisfies the forcing theorem for forcing over $M$. Then in the corresponding forcing extension $V$ of $M$ by $\P$, there is no elementary embedding $j:V\to M$ that is definable in $V$ from parameters.

Proof. Suppose not. Fix such a forcing notion $\P$ in $M$, defined by $\varphi(\cdot)$, and suppose that $j(x)=y$ is forced to be defined in $V$ by $\psi(x,y,\dot u)$.

Let $\kappa$ be least such that there is a condition forcing that in the forcing extension of $M$, there is a parameter $u$ for which the formula $\psi(x,y,u)$ defines an elementary embedding $j:V\to M$. This is expressible in the first-order language of set theory. Consequently, we have given a parameter-free definition of $\kappa$ in $M$. This contradicts the fact that $j:V\to M$ is an elementary embedding with critical point $\kappa$, since in this case $\kappa$ will not be in the range of $j$, but every definable element of $M$ will be in the range of $j$. Contradiction. QED

A similar argument works in the case that $\P$ is definable in $M$ from parameters below $\kappa$.

In the general case, let me now undertake a more general argument, in the case that $\P$ is definable by a formula $\psi(\cdot,z)$ using a parameter $z$, but I shall use an extra assumption. Specifically, I want it to be first-order expressible in a parameter $z'$, whether the class forcing notion defined by $\psi(\cdot,z')$ satisfies the forcing theorem and what is the forcing relation.

Theorem. Suppose that $\P$ is a ZFC-preserving class forcing notion definable from parameters in $M$ and satisfying the forcing theorem, such that the definition $\psi(\cdot,z)$ of $\P$ has the property that the property of whether $\psi(\cdot,z)$ defines such a class forcing notion with the forcing theorem is itself expressible in set theory, and the forcing relation is also definable from that parameter uniformly. Then in the forcing extension $V$ of $M$ by $\P$, there is no elementary embedding $j:V\to M$ that is definable in $V$ from parameters.

Proof. Let $\kappa$ be least among all parameters $z$ such that it is the critical point of such an embedding. Now we don't need the parameter $z$ to define $\kappa$ in $M$, and get the contradiction as before. QED

I'm not sure in general how to express that a definable class has the forcing theorem, uniformly in the parameter. Even in the case of pre-tame forcing, this seems to involve quantifying over arbitrary classes and has complexity $\Pi^1_1$ over $M$.