# Truth and Definability Lemmas

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.

• Congratulations on asking the 100th question about [forcing]. Nov 30, 2013 at 14:54
• @AsafKaragila: I did not realize that. Maybe the question should have been something deeper, seeing as it is the 100th question on Forcing. Nov 30, 2013 at 15:03
• You don't normally write $\Bbb N\models\ulcorner x\leq y\urcorner(0,1)$, do you now? Apr 7, 2014 at 0:25
• True. That is me being hyper pedantic. Apr 7, 2014 at 0:33
• OK. I think I get what you mean by your last comment. I was trying to be careful about the codes but there are a lot of different languages in the background (truth in M is related to L(M) etc) So many different types of coding done inside set theory itself. Anyway, I edited the question. Apr 7, 2014 at 11:41

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

• Thank you. I went ahead and added all three subscripts. If this is the way to think about the theorems then everything should be good. Nov 30, 2013 at 15:01
• @asafkaraglia I edited the question (after a really long time) by a bit. I still think the statements are correct though. Apr 7, 2014 at 0:24
• @Danul: As luck would have it, I saw the edits; but if you wish to ping me, either do it on a post where I have commented before, or on a post that I have authored. Not on Andreas' answer, that until now I haven't commented. Apr 7, 2014 at 0:27
• Oops. Sorry. I wanted to ping you both and StackExchange told me it would ping Andreas anyway since he authored the answer. Apr 7, 2014 at 0:33

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.