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