Visualización del forzamiento como resultado de modelos transitivos contables

Pienso en forzar en el siguiente contexto: Lemas de Verdad y Definibilidad . De modo que forzar es un esquema en la metateoría.

Ahora, en su libro Teoría de conjuntos (la primera edición), Kunen afirma que establecer el siguiente esquema también se ocupa de las matemáticas necesarias para mostrar$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)$

Aquí, para eliminar el uso de la relativización, podemos reemplazar las ocurrencias de$(\text{Forces}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})})^{M}$por$M\models\ulcorner\text{Forces}_{\varphi}^{*}\urcorner{[(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})]}$si queremos. Con eso estoy bien. Pero no estoy seguro de cómo podemos reemplazar el esquema forzado con un solo teorema dentro de$ZFC$(Tendría que hacer esto para verificar$N\models{\ulcorner{ZFC}\urcorner}$).

La "solución de seguir mi nariz" es decir que después de formalizar la lógica y la teoría del modelo dentro de la teoría de conjuntos, puedo probar (como lo señaló justus87 que ya no necesito mantener la notación de esquina ya que estoy demostrando un resultado sobre conjuntos dentro de la teoría de conjuntos.):

$ZFC\vdash\forall\varphi(x_{1},...,x_{n})\in{Fm_{L=\{\in\}}}$con todas las variables libres mostradas,$\exists\text{Forces}_{\varphi}^{*}(x_{1},...,x_{n},y_{1},...,y_{4})\in{Fm_{L=\{\in\}}}$calle$\forall$ctm$M\models{{ZF-P}}$,$\forall{\mathbb{(P,\leq,1)}}\in{M}$,$\varkappa_{1},...,\varkappa_{n}\in{M^{\mathbb{P}}}, \forall{G}$eso es$\mathbb{P}-$genérico sobre$M$,

a) Si$p\in{G}$y$M\models\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})}$entonces$M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$
b) Si$M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$, entonces hay$p\in{G}$calle$M\models\mbox{Forces}^{*}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})$

Esto parece correcto y debería seguir, pero no soy un$100\%$cierto. Escribir un esquema dentro de la meta-teoría como un teorema es algo complicado y no lo he dominado del todo (si intentamos hacer esto con los teoremas de reflexión y lo hacemos incorrectamente terminamos obteniendo que$ZFC$es inconsistente).

Edición 1: Me di cuenta de que tenía mal los símbolos de los códigos. Ahora en este caso los códigos serán los códigos para$L(M)$y$L(M[G])$

Edición 2: eliminé el uso de códigos después de formalizar la lógica y la teoría de modelos en ZFC. Mi idea inicial era que tendría los códigos originales para establecer fórmulas teóricas y al considerar fórmulas de$L(M)=L\cup{\{c_{m}:m\in{M}\}}$Podría extender los códigos de tal manera que los nuevos códigos ($\ulcorner\urcorner_{1}$) tenía la propiedad de que si$\ulcorner\phi\urcorner_{1}$símbolos utilizados sólo en$L$, entonces$\ulcorner\phi\urcorner_{1}=\ulcorner\phi\urcorner$. (Debería funcionar incluso sin eso, es decir, incluso si$L(M)$tiene códigos nuevos que no amplían los códigos antiguos, aún podemos insistir en que el nuevo código$\ulcorner\phi\urcorner_{1}$representa la fórmula que originalmente estaba representada por$\ulcorner\phi\urcorner$)