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?



Generic Ultrapower as a Class
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.


