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.