Viewing forcing as a result about countable transitive models

I think of forcing in the following context: Truth and Definability Lemmas. So forcing is a schema in the meta theory.

Now in his Set Theory book (the first edition), Kunen claims that setting up the following schema also deals with the mathematics required for showing $ZFC\vdash{\forall{\text{ctm } M \text{ of } {\ulcorner{ZFC}\urcorner}}} \implies \exists{N} (M\subseteq{N} \wedge N \text{ is a ctm of } \ulcorner{ZFC+\neg{CH}}\urcorner)$

Here in order to eliminate the use of relativization we can replace 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. That I'm fine with. But I'm not sure how to we can replace the forcing schema with a single theorem inside of $ZFC$ (I would need to do this to verify $N\models{\ulcorner{ZFC}\urcorner}$).

The "follow my nose solution" is to say that after formalizing logic and model theory inside of set theory I can prove (as pointed out by justus87 I don't need to keep the corner notation anymore since I'm proving a result about sets inside of set theory.):

$ZFC\vdash\forall\varphi(x_{1},...,x_{n})\in{Fm_{L=\{\in\}}}$ with all free variables shown, $\exists\text{Forces}_{\varphi}^{*}(x_{1},...,x_{n},y_{1},...,y_{4})\in{Fm_{L=\{\in\}}}$ s.t. $\forall$ ctm $M\models{{ZF-P}}$, $\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 $M\models\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})}$ then $M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$
b) If $M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$, then there is $p\in{G}$ s.t. $M\models\mbox{Forces}^{*}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})$

This looks correct and should follow but I'm not a $100\%$ certain. Writing a schema inside the meta-theory as a theorem is somewhat tricky and I haven't quite mastered it (if we try to do this with the reflection theorems and do it improperly we end up obtaining that $ZFC$ is inconsistent).

Edit 1: I realized that I had the symbols for the codes down wrong. Now in this case the codes will be the codes for $L(M)$ and $L(M[G])$

Edit 2: I removed the use of codes after I formalized logic and model theory in ZFC. My initial idea was I would have the original codes for set theoretic formulas and when considering formulas of $L(M)=L\cup{\{c_{m}:m\in{M}\}}$ I could extend the codes in such a way so that the new codes($\ulcorner\urcorner_{1}$) had the property that if $\ulcorner\phi\urcorner_{1}$ used symbols only in $L$, then $\ulcorner\phi\urcorner_{1}=\ulcorner\phi\urcorner$. (It should work even without that, i.e. even if $L(M)$ has new codes that does not extend the old codes we can still insist that the new code $\ulcorner\phi\urcorner_{1}$ represents the formula that was originally represented by $\ulcorner\phi\urcorner$)

-

If you formalize all the stuff in Kunen's presentation of forcing, you will get (in $\mathsf{ZFC}$) a map $\mathrm{Fm} \to \mathrm{Fm}, \ \phi \mapsto \mathrm{Forces}_\phi^*$.

So the main lemma says (as a theorem of $\mathsf{ZFC}$):

Let $n < \omega$. Let $M$ be a c.t.m. for $\ulcorner \mathrm{ZFC} \urcorner$ and let $\phi \in \mathrm{Fm}_n$ a formula with exactly $n$ free variables. Let $\mathbb{P} := (P, \leq, \mathbb{1}) \in M$ be a preorder with largest element. Let $\tau_0, \ldots, \tau_{n - 1} \in M^\mathbb{P}$ be names and $G \subseteq P$ a $\mathbb{P}$-generic filter over $M$.

(a) If $p \in G$ and $M \models \mathrm{Forces}_\phi^* [\tau_0, \ldots, \tau_{n - 1}, P, \leq, p]$, then $M[G] \models \phi[{\tau_0}_G, \ldots, {\tau_{n - 1}}_G]$.

(b) ... [similar] …

Note that $\ulcorner \mathrm{ZFC} \urcorner := \{ x \in \mathrm{Fm} : \chi_\mathsf{ZFC}(x) \}$ relies on choosing a meaningful representing formula $\chi_\mathsf{ZFC}$ in the meta-theory. (See IV §10 in Kunen's book (1980 edition)!)

For example, your statement does not make sense at these points:

• "$\exists \ulcorner \mathrm{Forces}_\varphi(x_1, \ldots, x_n, y_1, \ldots, y_4) \urcorner \in Fm_{L=\{\in\}}$" is not good because $\mathrm{Fm} \to \mathrm{Fm}, \ \phi \mapsto \mathrm{Forces}_\phi^*$ is a mapping (within $\mathsf{ZFC}$) now. So you must not use the Quine corners. These corners denote a formal representation of a meta-theoretical object - but that's what you want to avoid.

• "$M[G] \models \ulcorner \varphi({\varkappa_1}_G, \ldots, {\varkappa_n}_G) \urcorner$" should be "$M[G] \models \ulcorner \varphi \urcorner [{\varkappa_1}_G, \ldots, {\varkappa_n}_G]$" or better (for the same reason as above) "$M[G] \models \varphi [{\varkappa_1}_G, \ldots, {\varkappa_n}_G]$".

• etc.

Also remark that this forcing for the formal representation of $\mathsf{ZFC}$ yields $$\mathsf{ZFC} \vdash \forall M \ ((M \text{ is a c.t.m. for } \ulcorner \mathrm{ZFC} \urcorner) \longrightarrow \exists N \supseteq M \ (N \text{ is a c.t.m. for } \ulcorner \mathrm{ZFC} \urcorner \ \land \ N \models \ulcorner \mathrm{CH} \urcorner))$$ for example, but $$\mathsf{ZFC} \nvdash \exists M \ (M \text{ is a c.t.m. for } \ulcorner \mathrm{ZFC} \urcorner),$$ so the logical interpretation is different.

-
I'm not sure why you say that the first bullet doesn't make sense. It says that there is a particular formula in the language of set theory. For the second bullet point: I'm assuming that logic and model theory has been formalized inside of ZFC, so the code actually refers to a code in $L(M)$ (as you would do in Tarski definition of truth) with an underlying function to keep track of the fact that $\ulcorner\phi(\varkappa_{1},...\urcorner)$ is in fact $\phi$ with the correct things plugged in. (I wasn't really sure how to do this notationally so I might be wrong) – UserB1234 Apr 7 '14 at 15:49
Sorry, I don't get what you mean. What is $L(M)$ for you? And what is that "underlying function" you are talking of? If you formalized first-order logic within $\mathsf{ZFC}$, you do not need Quine corner notation anymore in the way you used it. – Justus87 Apr 8 '14 at 10:58
L(M) is the language $L\cup{\{c_{m}:m\in{M}\}}$ where the $c_{m}$ are constant symbols. This is the canonical language with which you can define truth inside of $M$ (you interpret $c_{m}$ as $m$)(This is how I was taught model theory). I see your comment about the corner notation. I kept using it because my question has both things (relativization and model theory) going on it at the same time which is why I still have the Quine notation. I'll change it back to match Kunen and I'll edit the question so as to reflect this. Thank you! – UserB1234 Apr 8 '14 at 11:42
Ah, I see. You're welcome! – Justus87 Apr 8 '14 at 21:24