Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question

2 Answers 2

up vote 6 down vote accepted

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.

share|improve this answer
I agree with this, and in any case, having a predicate for the ground model, as Jech does, also works fine, and avoids the need for localization. Nevertheless, to my way of thinking, the real answer to the question, "How does $M[G]$ talk about $M$?" is the ground model definability theorem. –  Joel David Hamkins Apr 15 at 13:32

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.

share|improve this answer
Joel, can you give some ideas/reference on how Laver-Woodin result is proved? –  Ashutosh Apr 15 at 0:27
@Ashutosh, I added some references. A complete proof is found in Laver's paper, and also in Reitz's work and elsewhere. –  Joel David Hamkins Apr 15 at 0:37
Thanks a lot! I am reading the pdf linked there now. –  Ashutosh Apr 15 at 0:38
I just wanted to note that it is still open whether ground model definability holds for models of just $ZF$. It is not known whether every forcing extension $M[G]$ of $M\models ZF$ can define $M$. –  Victoria Gitman Apr 15 at 18:27

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.