Who defined $P$-names? On reading Cohen's "Set Theory and the Continuum Hypothesis" it occurred to me that it might not have been Cohen himself who first defined $P$-names. In his book on page 113 he defines what he calls a "labeling" as follows:

Definition. A "labeling" is a mapping defined in ZF, which assigns to each ordinal $0 < \alpha < \alpha_0$, a set $S_\alpha$, the "label space", and functions $\varphi_\alpha$ defined in $S_\alpha$ such that the sets $S_\alpha$ are disjoint and if $c \in S_\alpha$, $\varphi_\alpha(c)$ is a formula $A(x)$ which has all its bound variables restricted to $X_\alpha$ and which may have elements of $S_\beta$ with $\beta < \alpha$ appearing as constants. The function $\varphi_\alpha$ must put $S_\alpha$ into one-one correspondence with the set of all such formulas. The set $S_0$ is defined as the set $\omega \cup \{a\}$ where $a$ is a formal symbol. ...

If I understand correctly this is Cohen's definition of what later became $P$-names. Hence my question: who first "invented" $P$-names?
 A: It might have been in

J.R. Shoenfield, Unramified forcing, in Proceedings of Symposia in Pure Mathematics Vol. XIII, Part I: Axiomatic Set Theory (D. Scott, ed., 1971), pp. 357–381

(though I am certainly ready to delete this answer if someone can find an earlier reference).
Therein we have the following:

We introduce a language, called the forcing language, which is suitable for discussing $M[G]$. The symbols of the forcing language are the symbols of ZFC and the elements of $M$.  Each element $a$ of $M$ is regarded as a constant which designates the element $\bar{a}$ of $M[G]$; we say $a$ is a name of $\bar{a}$.  If $\Phi$ is a sentence of the forcing language, $\vdash_G \Phi$ means that $\Phi$ is true in $M[G]$.

While this doesn't explicitly give the set of $P$-names as we know them today, the definition of the (weak-)forcing relation relation is quite similar to our own:

  
*
  
*$p \Vdash^* a \in b$ if $\exists c ( \exists q \geqq p ) ( \langle x , q \rangle \in b \;\&\; p \Vdash^* a = c )$.  
  
*$p \Vdash^* a \neq b$ if $\exists c ( \exists q \geqq p ) ( \langle c , q \rangle \in a \;\&\; p \Vdash^* c \notin b )$ or $\exists c ( \exists q \geqq p ) ( \langle c , q \rangle \in b \;\&\; p \Vdash^* c \notin a )$
  

Thus we clearly have that the sets which are $P$-names in our current sense are the important ones.
Even the construction (made earlier in the paper) of the generic extension is essentially the modern one:

Now suppose that $C$ s a notion of forcing in a countable model $M$ of ZFC and that $G$ is $C$-generic over $M$.  We are going to construct an extension of $M$ containing $G$.  
We shall first define a structure which has universe $M$ but has a new membership relation $\in_G$ defined by
  $$a \in_G b \leftrightarrow ( \exists p \in G ) ( \langle a , p \rangle \in b ).$$
  ... We then use the collapsing technique to convert $\langle M , \in_G \rangle$ into a transitive model.  We first note that
  $$a \in_G b \rightarrow a \in \mathrm{Ra}(b)$$
  and hence
  $$a \in_G b \rightarrow \mathrm{rk}(a) < \mathrm{rk}(b). \tag{4.2}$$
  We then define $$K_G ( b ) = [ K_G ( a ) : a \in_G b ].$$  By (4.2), this is a legitimate definition by induction on $\mathrm{rk}(b)$.  Finally, we define $$M[G] = [ K_G(a) : a \in M ].$$

A: This is less of an answer on its own, and more of a circumstantial evidence to support Arthur's answer (as well my own original intuition), that the idea and modern definition of $P$-names is due to Shoenfield.
I am looking at "Measurable cardinals and the continuum hypothesis" by Solovay and Levy which was written in 1967, after the never-published Scott-Solovay paper was already circulating (they refer to it in the introduction). There is no mention of names, nor unramified forcing in any sense.
However there is a reference to an abstract class of terms to which there is an injection from the class of all sets, this would later be the map $x\to\check x$. It is also pointed out that every set in the generic extension (although this terminology do not appear there) has a term which represents it.
From the several historical overviews I read in the past two hours I can tell that it was Shoenfield who engineered the idea of forcing with arbitrary models of ZF using partial orders. So while there might be a slim chance that Scott and Solovay did come up with the idea of $P$-names as we know them (as Solovay was the one who noted that we can really just do forcing with partial orders) in between 1967 to 1970, it still seems more reasonable that Shoenfield was the one to come up with that idea.
Even more evidential is that in 1970 when Solovay published his famous "A model of set-theory in which every set of reals is Lebesgue measurable." he did not use the modern definition of $P$-names (although it seemed that the Scott-Solovay paper would appear that summer, despite no further references to such publications are to be found).
It would be a good estimate, if so, to conclude that Shoenfield in his "Unramified forcing" came up with the definition.
