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.