Viewing forcing as a result about countable transitive models

Question

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

Answer 1

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.