Forcing Language I asked the following question (slightly paraphrased) about a week ago in Stack exchange but no one knew the answer to the particular question. I was hoping someone here might be able to help me.
"Does anyone know of a reference that explains the concept of forcing by fixing a forcing language that has a (I believe unary) predicate and does not mention the forcing poset?
For example, Kunen's development will have no one fixed forcing language. It will have a class of forcing languages, for each forcing poset $\mathbb{P}$. The development I'm thinking of will fix the forcing language and will deal with details through the unary predicate. So instead of a class of languages we have one language to handle the details.
(I realize that the question is vague and I apologize for it)" 
The link to the question in Stack Exchange is: https://math.stackexchange.com/questions/556171/forcing-language
 A: $\newcommand\P{\mathbb{P}}\newcommand\B{\mathbb{B}}$
Now I understand what you want. 
The usual account of forcing has an explosion in the size of the official language, by adding all the $\P$-names as official terms to the language. And not only does this make the language a proper class, but as you point out it also makes the choice of forcing language dependent on which forcing notion $\P$ will be used. Perhaps one might find this regrettable. 
Meanwhile, one may easily undertake forcing in an alternative set-up along the lines you describe, having only the language of set theory as the official language, and perhaps adding a unary predicate for the ground model, if you like. 
With this way of doing it, one views the names as the semantic objects constituting the model that is constructed, rather than as syntactic objects in the forcing language. But in truth, everything works out essentially the same and this different perspective doesn't really change any of the analysis. For any particular forcing notion $\B$, a complete Boolean algebra, one builds the universe $V^\B$ as a Boolean-valued model in that forcing language. What is a Boolean valued model? Well, it is a collection of objects, called names, together with a truth-value assignment $[[\sigma=\tau]],[[\sigma\in\tau]]\in\B$, which respects the laws of equality, in the sense that $[[\sigma=\sigma']]\wedge[[\tau=\tau']]\wedge[[\sigma\in\tau]]\leq [[\sigma'\in\tau']]$. One then extends the Boolean values inductively so that $[[\varphi\wedge\psi(\vec\sigma)]]=[[\varphi(\vec\sigma)]]\wedge[[\psi(\vec\sigma)]]$ and so on as usual. The predicate for the ground model, whcih I usually call $\check V$, is defined by $[[\tau\in\check V]]=\sup\{[[\tau=\check x]]\mid x\in V\}$. 
The only difference from the usual account is that now we are regarding $\varphi(\vec \sigma)$ as a substitution instance of a formula with free variables that have have been subsituted at the point $\vec\sigma$ in the model, rather than regarding $\varphi(\vec\sigma)$ as a sentence in the forcing language. This is an essentially invisible distinction, which doesn't affect any of the theory.
