MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am a beginner of forcing, often I read from some articles something like "$p \Vdash \dot{G}$ is $P$-generic over $\check{M}$" (where $M$ is a countable transitive model, for instance).

Q1. I learnt from Jech's book a definition of "$p \Vdash \dot{x} \in \check{M}$", but I don't know how to translate "$p \Vdash \dot{G}$ is $P$-generic over $\check{M}$" into a formal version using this.

Q2. I also learnt from Kanamori's book that M is a definable proper class of $M[G]$ whenever $G$ is generic over $M$, why definable (i.e. of the form $\lbrace x \in M[G]: \phi(x) \rbrace$)?

share|cite|improve this question
Could you use TeX? – Martin Brandenburg Oct 21 '11 at 11:55
Sorry, I forgot to add $. – sonicyouth Oct 21 '11 at 14:21
up vote 6 down vote accepted

In the Boolean-value approach to forcing, one may introduce a new predicate symbol $\check M$ into the forcing language, and then define that $[[\tau\in\check M]]=\bigvee_{x\in M}[[\tau=\check x]]$. That is, the Boolean value that $\tau$ is in $\check M$ is precisely the extent to which it is equal to something in the ground model. This definition obeys the equality axioms, and so one may expand the forcing language to include this new predicate for the ground model.

The forcing relation $p\Vdash\varphi$ just means $p\leq[[\varphi]]$, identifying the condition $p$ with its copy in the Boolean algebra, and therefore $p\Vdash\tau\in\check M$ just means that $p\leq[[\tau\in\check M]]$ as I defined it above. One may avoid the use of Boolean values via the equivalent formulation:

  • $p\Vdash\tau\in\check M$ if and only if the set of $q$ for which there is $x\in M$ with $q\Vdash\tau=\check x$ is dense below $p$.

It follows that whenever $G$ is $M$-generic for $P$, then the collection of $\text{val}(\tau,G)$ for which $p\Vdash\tau\in\check M$ is precisely the same as $\text{val}(\check x,G)=x$ for $x\in M$. That is, the interpretation of $\check M$ by a generic filter $G$ is precisely $M$, which is as it is desired.

For your second question, my belief is that the definability of the ground model $M$ in its set forcing extensions $M[G]$ was a recent theorem due to Richard Laver, in his paper Certain very large cardinals are not created in small forcing extensions, using a proof that is due to me, and was also observed independently by W. Hugh Woodin. This theorem is the starting point of the subject of Set-theoretic geology, which I introduced with Jonas Reitz and Gunter Fuchs, as well as J. Reitz's work on The Ground axiom. The point of this theorem is that one needn't actually introduce the predicate $\check M$, as the class that it picks out is a definable class (using parameters) in the language of set theory. To which theorem of Kanamori's book do you refer?

If you don't have parameters, then it is not true generally that the ground model $M$ is definable in the forcing extension $M[G]$. One way to see this is to add two mutually generic Cohen reals $c$ and $d$, and consider the extension $M[c][d]$, which is a forcing extension of $M$, of $M[c]$ and of $M[d]$. If $M[c]$ were a parameter-free definable class of $M[c][d]$, then the set of reals of $M[c]$ would be a parameter-free definable set in $M[c][d]$, and hence in the HOD of $M[c][d]$. But the forcing is ordinal-definable and homogeneous, and so the HOD of $M[c][d]$ must be contained in $M$, a contradiction. Thus, $M[c]$ is not a parameter-free definable class in $M[c][d]$. But it is definable with parameters, and it is also (trivially) definable in the language where you have added a predicate for the ground model. Perhaps it is this latter situation to which you refer.

share|cite|improve this answer
Thank you! on line -3, page 118, Kanamori's book, it is wrote that "the ground model can be considered a (definable) class, and hence an inner model, in any generic extension." Is it correct? – sonicyouth Oct 26 '11 at 2:04
He specifically says on that page that he does not adopt any particular formalism. One interpretation of what he writes is that the ground model is definable in the language with the new predicate for the ground model, as I explain in the first part of my answer, and this reading is supported by the fact that he says it is definable "by this means" that is, by means of the names $\check x$. He doesn't argue there that the ground model is definable (from parameters) in the language without that predicate, but Laver's theorem shows that this is correct. (It's not correct without parameters.) – Joel David Hamkins Oct 26 '11 at 12:52
I wrote to Aki, who confirmed that he meant that the ground model would be definable in the forcing extension using the predicate for the ground model. But meanwhile, the Laver/Woodin theorem shows that it is definable from parameters even in the ordinary language of set theory. – Joel David Hamkins Oct 26 '11 at 14:24
Thanks again, does it mean M can be defined in M[G] by $x\in M$ iff $\phi(x, V_{\delta+1})$ where $\phi$ is a formula and $\delta$ as defined in Theorem 3(Laver's paper)? And so that we can avoid "$p\Vdash\tau\in\check M$" by saying "$p\Vdash\phi(\tau, V_{\delta+1} \check)$"? – sonicyouth Nov 9 '11 at 1:32
Yes. The definition also appears explicitly written out in Jonas Reitz's work on the ground axiom. – Joel David Hamkins Nov 10 '11 at 17:25

Just to dot an i and/or cross a t in Joel's answer, since you asked about formalizing "$p$ forces "$\dot G$ is generic over $\check M$": Notice that, once you've introduced $\check M$ as a predicate symbol in the forcing language, as in Joel's answer, you can use it to write the usual definition of genericity as a sentence in the forcing language. The crucial clause (the only one involving $\check M$) is $$(\forall D\subseteq \check P)[(D \text{ dense in }\check P)\land (D\in\check M)\implies (D\cap\dot G\neq\emptyset)].$$

Let me also point out something implicit in Joel's choice of expository method: Foundational things about forcing, like this, tend to be more natural and easier to understand if you think in terms of Boolean-valued models. If necessary, you can then translate into the terminology of forcing. The value of forcing (as opposed to Boolean-valued models) is not in foundational matters but rather in explicit constructions; it's usually (though not always) easier to describe a notion of forcing than to describe its associated compete Boolean algebra.

share|cite|improve this answer

In most cases, however, you can get rid of the problem of referring to $\check{M}$. Andreas' formula above, for example, can be written as $$ (\forall D)((D\in \check{X})\Longrightarrow (D\cap \dot{G}\neq\emptyset)). $$ where $X$ is the set of dense subsets of $P$ (as defined in $M$).

Another standard trick to ensure that $M$ is a definable class in $M[G]$ is to force over $L$ (whenever one can, this clearly rules out the use of some large cardinals).

share|cite|improve this answer
Thank you! But, in fact I met a problem in Kunen's article "Random and Cohen reals" (see Handbook of Set-Theoretic Topoloy),that is, suppose $I \in M$ and $F\in 2^{I}$ is random over M, $J,K\in M$ and I is a disjoint union of J and K, try to prove the restriction of F on K is random over N, where N is the model by adding the restriction of F on J(I have seen that F|J is random over M) to M. – sonicyouth Oct 26 '11 at 2:07
As the proof of Theorem 3.13 (2nd paragraph of the proof), let g be a name for generic filters, try to prove 1 forces "the restriction of g on K is random over M[g|J]". How to formalize the sentence (1 forces "the restriction of g on K is random over M[g|J]")? – sonicyouth Oct 26 '11 at 2:07

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.