Defining forcing relation in base transitive model $M$

Question

In page 177 of Set Theory for the Working Mathmatician, on chapter forcing it says:

Theorem 9.2.7 For every formula $\varphi(x_1,..., x_n)$ of set theory there exists another formula $\psi(\pi,P,x_1,...,x_n)$, denoted by $\pi \Vdash_{\mathbb{P}}^{*} \varphi(x_1,...,x_n)$, such that for every countable transitive model $M$ of ZFC, partial order $\mathbb{P} \in M$, and $\mathbb{P}$-names $\tau_1,...,\tau_n \in M$ $$p \Vdash_{\mathbb{P},M} \varphi(\tau_1,...,\tau_n) \Leftrightarrow M \models (p \Vdash_{\mathbb{P}}^{*} \varphi(\tau_1,...,\tau_n))$$ for every $p \in \mathbb{P}$.

The proof of this theorem is not presented, and I would like to know what the proof would be.

Answer 1

We can define this by induction on the complexity of $\varphi$.$\DeclareMathOperator{rank}{rank}\newcommand{\forces}{\Vdash}$

Atomic formula. Note that there are two types of atomic formulas in the language of set theory, $x\in y$ and $x=y$. We define both at the same time by induction on the [maximum of the] rank of the names $\tau_x$ and $\tau_y$. Assume that we have defined the wanted formula for ranks below $\max\{\rank(\tau_x),\rank(\tau_y)\}$.

1. We say that $p\forces^*\tau_x=\tau_y$ if for every $\langle s,\tau_u\rangle\in\tau_x$ the following set is dense below $p$: $$\{q\mid q\leq s\rightarrow\exists\langle r,\tau_v\rangle\in\tau_y:q\leq r\land q\forces^*\tau_u=\tau_v\}$$ and similarly for every $\langle r,\tau_v\rangle\in\tau_y$.

2. We say that $p\forces^*\tau_x\in\tau_y$ if the following set is dense below $p$ $$\{q\mid \exists\langle r,\tau_v\rangle\in\tau_y:q\leq r\land q\forces^*\tau_x=\tau_v\}.$$

(Note that I am forcing downwards, which may or may not be compatible with your definition of forcing; and that the requirement that these sets are dense below $p$ can be written explicitly that every $q\leq p$ has some $r$ which is compatible with $q$/stronger than $q$ such that $r\forces\ldots$)

Connectives. It's quite straightforward in the case of conjunction, $p\forces^*\varphi\land\psi$ if $p\forces^*\varphi$ and $p\forces^*\psi$.

Negation. We say that $p\forces^*\lnot\varphi$ if there is no $q\leq p$ such that $q\forces^*\varphi$.

Existential quantifier. We say that $p\forces^*\exists x\varphi(x)$ if the following set is dense below $p$: $$\{q\mid\exists\tau_x:q\forces^*\varphi(\tau_x)\}$$

---

This can be translated into a single uniform formula $\psi$ as wanted. To see that the definition given above, and the definition by generic filters

$p\forces\varphi\iff M[G]\models\varphi$ for every $M$-generic $G$ such that $p\in G$.

The equivalence between $\forces$ and $\forces^*$ is proved by induction on the formulas, and heavy use of the fact that if $p\in G$ and $G$ is generic, then $G$ meets every dense set below $p$.