# 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

• Can you explain more what you want? You want a single forcing language in which it makes sense to define the forcing relation (or Boolean values) for any forcing notion? What is the unary predicate for?One could of course make such a language artificially, but what specific properties do you want for your set-up? One can develop forcing naturally in the language of set theory itself, without regarding the names as synactic objects in the language; instead, one views the names as providing elements of a model in that language. Is that what you are wanting? – Joel David Hamkins Nov 13 '13 at 14:18
• The idea in Kunen is something like this: Once you fix a $\mathbb{P}$ then you have a class sized forcing language $L_{\mathbb{P}}$ inside of set theory. Now $M[G]$ has a canonical interpretation as an $L_{\mathbb{P}}\cap{M}$ structure which works out nicely. What I want is something like this. Fix one forcing language $\{\epsilon, =, U\}$. Now using facts like: for any $M$ a ctm of $ZFC$ and $\mathbb{P}\in M$ the $\mathbb{P}$ names of $M$ are definable in $M$, get the unary predicate to relate $M$ and $M[G]$. This way we need only one forcing language. I think this has been used before. – UserB1234 Nov 13 '13 at 16:03

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