Forcen als Ergebnis über zählbare transitive Modelle anzeigen

An Forcen denke ich in folgendem Kontext: Wahrheits- und Definierbarkeits-Lemmas . Forcieren ist also ein Schema in der Metatheorie.

Jetzt behauptet Kunen in seinem Buch Mengenlehre (der ersten Ausgabe), dass das Aufstellen des folgenden Schemas sich auch mit der Mathematik befasst, die zum Zeigen erforderlich ist$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)$

Um die Verwendung von Relativierungen zu eliminieren, können wir hier die Vorkommen von ersetzen$(\text{Forces}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})})^{M}$von$M\models\ulcorner\text{Forces}_{\varphi}^{*}\urcorner{[(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})]}$wenn wir wollen. Damit bin ich einverstanden. Aber ich bin mir nicht sicher, wie wir das erzwingende Schema durch ein einzelnes Theorem innerhalb von ersetzen können$ZFC$(Ich müsste dies tun, um dies zu überprüfen$N\models{\ulcorner{ZFC}\urcorner}$).

Die "Folge meiner Nase Lösung" ist zu sagen, dass ich nach der Formalisierung von Logik und Modelltheorie innerhalb der Mengenlehre beweisen kann (wie von justus87 betont, muss ich die Ecknotation nicht mehr behalten, da ich ein Ergebnis über Mengen beweise innerhalb der Mengenlehre.):

$ZFC\vdash\forall\varphi(x_{1},...,x_{n})\in{Fm_{L=\{\in\}}}$mit allen freien Variablen angezeigt,$\exists\text{Forces}_{\varphi}^{*}(x_{1},...,x_{n},y_{1},...,y_{4})\in{Fm_{L=\{\in\}}}$st$\forall$ctm$M\models{{ZF-P}}$,$\forall{\mathbb{(P,\leq,1)}}\in{M}$,$\varkappa_{1},...,\varkappa_{n}\in{M^{\mathbb{P}}}, \forall{G}$das ist$\mathbb{P}-$generisch vorbei$M$,

a) Wenn$p\in{G}$Und$M\models\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})}$Dann$M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$
b) Wenn$M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$, dann ist da$p\in{G}$st$M\models\mbox{Forces}^{*}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})$

Das sieht korrekt aus und sollte folgen, aber ich bin kein$100\%$bestimmt. Ein Schema innerhalb der Metatheorie als Theorem zu schreiben ist etwas schwierig und ich habe es nicht ganz gemeistert (wenn wir versuchen, dies mit den Reflexionstheoremen zu tun und es nicht richtig machen, erhalten wir das am Ende$ZFC$ist widersprüchlich).

Bearbeiten 1: Mir ist aufgefallen, dass ich die Symbole für die Codes falsch geschrieben habe. In diesem Fall sind die Codes nun die Codes für$L(M)$Und$L(M[G])$

Bearbeiten 2: Ich habe die Verwendung von Codes entfernt, nachdem ich Logik und Modelltheorie in ZFC formalisiert hatte. Meine ursprüngliche Idee war, dass ich die ursprünglichen Codes für mengentheoretische Formeln und bei der Betrachtung von Formeln haben würde$L(M)=L\cup{\{c_{m}:m\in{M}\}}$Ich könnte die Codes so erweitern, dass die neuen Codes ($\ulcorner\urcorner_{1}$) hatte die Eigenschaft, dass wenn$\ulcorner\phi\urcorner_{1}$verwendete Symbole nur in$L$, Dann$\ulcorner\phi\urcorner_{1}=\ulcorner\phi\urcorner$. (Es sollte auch ohne das funktionieren, also auch wenn$L(M)$hat neue Codes, die die alten Codes nicht erweitern, können wir immer noch darauf bestehen, dass der neue Code$\ulcorner\phi\urcorner_{1}$stellt die Formel dar, die ursprünglich durch dargestellt wurde$\ulcorner\phi\urcorner$)