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.

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.

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]$.

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.