Wahrheits- und Definierbarkeits-Lemmas

Ich bin etwas verwirrt über Wahrheits- und Definierbarkeits-Lemmata (manchmal auch Forcing Theorem A und Forcing Theorem B genannt) des Forcens. Ich habe Kunens neuen Text verwendet und aufgrund seiner Bemerkungen zu diesem Thema denke ich, dass er als Schema in der Metatheorie wie folgt verstanden werden sollte:

Lassen$\varphi(x_{1},...,x_{n})$Bohne$L=\{\in\}$Formel mit allen freien Variablen angezeigt. Dann gibt es eine Formel$\mbox{Forces}^{*}_{\varphi}(y_{1},..,y_{4},x_{1},...,x_{n})$mit$n+4$freie Variablen, die behauptet$(y_{1},y_{2},y_{3})$ist ein zwingender Poset$y_{4}\in{y_{1}}$,$x_{1},...,x_{n}\in{V^{y_{1}}}$Und$y_{4}\Vdash^{*}_{y_{1},y_{2},y_{3}}{\varphi(x_{1},...,x_{n})}$unter denen die Lemmata werden:

($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}$das ist$\mathbb{P}-$generisch vorbei$M$,

a) Wenn$p\in{G}$Und$(\mbox{Forces}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n}))^{M}$Dann$M[G]\models\ulcorner\varphi\urcorner{[({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})]}$
b) Wenn$M[G]\models\ulcorner\varphi\urcorner{[({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})]}$, dann ist da$p\in{G}$st$(\mbox{Forces}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n}))^{M}$

Ist mein Verständnis richtig oder übersehe ich hier etwas? So wie ich es formuliert habe, gibt es eine gewisse Redundanz im Theorem (die Tatsache, dass$\mathbb{P}$ist ein zwingender Poset, der zweimal erscheint). Liegt das daran, dass ich etwas verpasst habe?

Edit: Ich habe die hinzugefügt$\ulcorner$,$\urcorner$Symbole, da dies die richtige Schreibweise sein sollte. Ich glaube auch, dass ich recht habe, wenn ich sage, dass wir die Verwendung von Relativierungen eliminieren können, indem wir die Vorkommen von ersetzen$(\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})})^{M}$von$M\models\ulcorner\text{Forces}^{*}_{\varphi}\urcorner{[(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})]}$wenn wir wollen.