"name" for the ground model

Question

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$)?

Answer 1

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.

Answer 2

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.

Answer 3

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).