# 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 '13 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 '13 at 15:03
• You don't normally write $\Bbb N\models\ulcorner x\leq y\urcorner(0,1)$, do you now? Apr 7 '14 at 0:25
• True. That is me being hyper pedantic. Apr 7 '14 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 '14 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 '13 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 '14 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 '14 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 '14 at 0:33

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

• The problem is when I want to show: math.stackexchange.com/questions/742900/… Now relativization will not be enough: You do need actual model theory Apr 7 '14 at 15:53
• It is not that easy. You cannot just replace all relativized formulas with the corresponding model relations. To do forcing inside the formal representation, see my answer in your respective post. Apr 8 '14 at 10:32