Generic Ultrapower as a Class

Question

If $X$ is a set and $I$ is an ideal on $X$. Let $\mathbb{P}$ be the forcing poset consisting of $I^+$ subsets of $X$ with the subset partial ordering. Let $G$ be $\mathbb{P}$-generic filter over $M$, where $M$ is the ground model.

As in Jech Lemma 22.13, it can be shown that $G$ is a $M$-ultrafilter on $X$. I presume this means that in $M[G]$, it is proved that $G$ is $M$-ultrafilter.

Then the generic ultrapower is defined in $M[G]$ as follows : it consist of the equivalence classes of function $f : X \rightarrow M$ with $f \in M$ under the usual ultrapower equivalence relation with $\in^{Ult_G(M)}$ defined in the usual way.

I would like to think of the generic ultrapower as a class model in $M[G]$, but it is not immediately clear that it is definable.

The first issue is how exactly is Lemma 22.13 phrased in $M[G]$. How does $M[G]$ talk about $M$?

Then in the construction of the ultrapower, the equivalence class can of course be made into sets by considering element of least rank in each class. However, $M[G]$ still needs to distinguish those $f : X \rightarrow M$ which are in the ground models. Again, the main issue here seems to be whether $M$ is an inner model of $M[G]$.

I am vaguely aware of some result about $M$ being in some sense definable in $M[G]$? I do not know the result precisely to be able to tell if this result could be used to think of the generic ultrapower as a proper class. Nevertheless, it seems that Solovay used the generic ultrapower well before this result was known. How did he handle the definability issue of the generic ultrapower?

Answer 1

I think it is historically important to see that the earlier results involving generic ultrapowers, such as those of Solovay in the late 1960s, did not depend on the far-future realizations of Laver and Woodin. The Laver/Woodin result is important and interesting, but it seems that the known applications of generic ultrapowers can be formally justified by localization rather than appeal to the definability of the ground model.

It seems that applications of generic embeddings can always be obtained by considering some initial segment of the universe. For example, let's consider the result of Jech-Prikry that if there is an $\omega_2$-saturated ideal on $\omega_1$, then there are no Kurepa trees. Let $\theta$ be a sufficiently large regular cardinal, say much bigger than say $2^{2^{\omega_1}}$. Then $G$ is generic over $V$ iff $G$ is generic over $H_\theta$. Also, $\theta$ can be taken large enough that the ultrapower $H_\theta^{\omega_1}/G$ is well-founded iff the ultrapower of $V$ is.

The argument that there are no Kurepa trees goes by considering $j(T)$ where $T$ is some $\omega_1$-tree. If it is Kurepa, then $j(T)$ has $\omega_2^V$ nodes at level $\omega_1^V$. This is impossible if $\omega_2^V$ is a cardinal in $V[G]$, since $j(\omega_1^V) = \omega_2^V$, and the levels of $j(T)$ have size less than $j(\omega_1) = \omega_2^V$.

It is not hard to convince yourself that this argument can be carried out by considering generic ultrapowers of $H_\theta$, which can obviously be referred to in $V[G]$. The general lesson is that almost always, such metamathematical issues can be resolved in a similar way. Verifying a local property usually depends only on another local property. Purported counterexamples should be carefully examined.

Answer 2

I believe that in Jech's forcing formalism, he has a predicate for the ground model, so there is officially a predicate for $M$ in the forcing language used in $M[G]$. But actually, it is a theorem of Laver and Woodin that the ground model $V$ is a definable class in any set forcing extension $V[G]$. So we don't actually need the predicate for $M$, since it is a definable class in $M[G]$.

R. Laver, Certain very large cardinals are not created in small forcing extensions. Ann. Pure Appl. Logic 149 (2007), no. 1-3, 1–6. See also this answer to the question of whether the ground model definability theorem extends to class forcing, which gives an idea of how the result is proved.

After hearing about Laver's theorem, Jonas Reitz and I used his idea to formalize the Ground Axiom, which asserts that the universe is not obtained by set forcing. Although this statement appears at first to be a second-order assertion, quantifying over the possible ground models of the univese, in fact this axiom is expressible in the first-order language of set theory, as Jonas proved in his dissertation.

The ground model definability theorem is the first theorem of set-theoretic geology.