Truth and Definability Lemmas

Question

I'm slightly confused about truth and definability lemmas (sometimes called forcing theorem A and forcing theorem B) of forcing. I've been using Kunen's new text and from his remarks in the matter I think it should be understood as a schema in the meta-theory as follows:

Let $\varphi(x_{1},...,x_{n})$ be an $L=\{\in\}$ formula with all free variables shown. Then there is a formula $\mbox{Forces}^{*}_{\varphi}(y_{1},..,y_{4},x_{1},...,x_{n})$ with $n+4$ free variables that asserts $(y_{1},y_{2},y_{3})$ is a forcing poset $y_{4}\in{y_{1}}$, $x_{1},...,x_{n}\in{V^{y_{1}}}$ and $y_{4}\Vdash^{*}_{y_{1},y_{2},y_{3}}{\varphi(x_{1},...,x_{n})}$ under which the lemmas become:

($ZFC\vdash$)$\forall$ ctm $M\models{\ulcorner{ZF-P}\urcorner}$, $\forall{\mathbb{(P,\leq,1)}}\in{M}$, $\varkappa_{1},...,\varkappa_{n}\in{M^{\mathbb{P}}}, \forall{G}$ that is $\mathbb{P}-$generic over $M$,

a) If $p\in{G}$ and $(\mbox{Forces}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n}))^{M}$ then $M[G]\models\ulcorner\varphi\urcorner{[({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})]}$
b) If $M[G]\models\ulcorner\varphi\urcorner{[({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})]}$, then there is $p\in{G}$ s.t. $(\mbox{Forces}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n}))^{M}$

Is my understanding correct or am I missing something here? The way I've phrased there is some redundancy in the theorem (the fact that $\mathbb{P}$ is a forcing poset appears twice). Is this because I missed something?

Edit: I have added the $\ulcorner$, $\urcorner$ symbols since that should be the most proper way to write it. I also believe that I'm correct in saying that we can eliminate the use of relativization by replacing the occurrences of $(\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})})^{M}$ by $M\models\ulcorner\text{Forces}^{*}_{\varphi}\urcorner{[(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})]}$ if we want.

Answer 1

What you wrote looks OK except for one quibble: Since you use all three of $y_1,y_2,y_3$ to represent the forcing poset, all three (not just $y_1$) should technically be in the subscript of $\Vdash$ in the explanation of what you mean by $\text{Forces}_\varphi$.

Answer 2

I am answering to revision 8 of your question.

In my opinion, your elimination of some (Why not all?) relativized formulas does not make the forcing theorems any "better" (easier, more elementary, clearer) as you have to formalize FOL and the model relation inside $ \mathsf{ZF} $. The relativization is much more simple and clear. You need the meta-theory anyway!

So the forcing theorem is a meta-theoritical fact: For each sufficiently large finite fragment $ \psi_1, \ldots, \psi_m $ of $ \mathsf{ZFC} $ and for each formula $ \phi(x_1, \ldots, x_n) $, we have $$ \mathsf{ZFC} \vdash \forall M \left( \left( \lvert M \rvert = \aleph_0 \ \land \ M = \operatorname{trcl}(M) \ \land \ \bigwedge_{i = 1}^m \psi_i^M \right) \quad \longrightarrow \quad \forall (P, {\leq}, \mathbb{1}) \in M \quad [\ldots] \quad \left( \mathrm{Forces}_\phi(\ldots) \longleftrightarrow \mathrm{Forces}^*_\phi(\ldots)^M \right) \right), $$ if $ \mathrm{Forces}_\phi $ is defined by $ [\ldots] $ and $ \mathrm{Forces}^*_\phi $ is defined by $ [\ldots] $.

On the other hand, you can do all the stuff within $ \mathsf{ZFC} $ (if you want to get rid of all the "inexact" meta-theory), but you will never be able to prove (within $ \mathsf{ZFC} $) $$ \exists (M, E) \ (M, E) \models \ulcorner \mathrm{ZFC} \urcorner $$ unless $ \mathsf{ZFC} $ is inconsistent.

I cannot explain it any better than Kunen himself. So you might read VII §9 Other approaches and historical remarks of Kunen's book (1980 edition).