Kunen says about Forcing : The first step is to define M [G]. Roughly, this will be the set of all sets which can be constructed from G by applying set-theoretic processes definable in M. Each element of M[G] will have a name in M, which tells how it has been constructed from G.
Then the names are defined as :
$ \tau$ is a P-name iff $\tau$ is a relation and :
$$\forall <\sigma , p> \in \tau \text{ } [ \sigma \text{ is a P-name} \land p \in P]$$
So the question is : How does a P-name tell how it has been constructed from G, in terms of expressions in the language of set theory? So what is the link between a P-name and all set theory expressions, for example :
{ r } $\cup$ G ; {r} $\cap$ G ; G - { r } ; P - G etc..
So is there a proof that ALL Set Theory expressions involving G are included in some P-name ?