2
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ Congratulations on asking the 100th question about [forcing]. $\endgroup$
    – Asaf Karagila
    Nov 30 '13 at 14:54
  • $\begingroup$ @AsafKaragila: I did not realize that. Maybe the question should have been something deeper, seeing as it is the 100th question on Forcing. $\endgroup$
    – UserB1234
    Nov 30 '13 at 15:03
  • $\begingroup$ You don't normally write $\Bbb N\models\ulcorner x\leq y\urcorner(0,1)$, do you now? $\endgroup$
    – Asaf Karagila
    Apr 7 '14 at 0:25
  • $\begingroup$ True. That is me being hyper pedantic. $\endgroup$
    – UserB1234
    Apr 7 '14 at 0:33
  • $\begingroup$ 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. $\endgroup$
    – UserB1234
    Apr 7 '14 at 11:41
3
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – UserB1234
    Nov 30 '13 at 15:01
  • $\begingroup$ @asafkaraglia I edited the question (after a really long time) by a bit. I still think the statements are correct though. $\endgroup$
    – UserB1234
    Apr 7 '14 at 0:24
  • $\begingroup$ @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. $\endgroup$
    – Asaf Karagila
    Apr 7 '14 at 0:27
  • $\begingroup$ Oops. Sorry. I wanted to ping you both and StackExchange told me it would ping Andreas anyway since he authored the answer. $\endgroup$
    – UserB1234
    Apr 7 '14 at 0:33
0
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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 $\endgroup$
    – UserB1234
    Apr 7 '14 at 15:53
  • $\begingroup$ 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. $\endgroup$
    – Justus87
    Apr 8 '14 at 10:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.