Lo que está haciendo es describir un procedimiento que, dentro de $V$ , aísla la clase $WF$ . Hasta ahora, no estamos utilizando $CON(ZF-Reg)$ . Pero ten en cuenta que hasta ahora no hemos concluido $CON(ZF)$ o bien.
Ahora, supongamos que $CON(ZF-Reg)$ . Esto significa (por el teorema de completitud) que existe un modelo (conjunto) $M$ de $ZF-Reg$ . Pero entonces su procedimiento muestra cómo se puede identificar una subcolección $WF^M$ de $M$ que es un modelo de $ZF$ . Así que, ahora, tienes $CON(ZF)$ .
También hay una forma de argumentar sintácticamente que evita el teorema de completitud: Supongamos que $CON(ZF)$ falla. Esto significa que hay una prueba de una contradicción $\psi\land\lnot\psi$ de los axiomas de ZF. Esta prueba utiliza sólo un número finito de axiomas, digamos $\phi_1,\dots,\phi_n$ . La prueba de que la clase $WF$ es un modelo de $ZF$ es en realidad un metateorema: Para cada axioma $\phi$ de $ZF$ puede identificar una colección finita $T_\phi$ de los axiomas de $ZF-Reg$ que implican que $WF$ es un modelo de $\phi$ o más exactamente, $T_\phi$ demuestra la fórmula relativizada $\phi^{WF}$ . Utilizando propiedades básicas de las relativizaciones como $(\psi\to\rho)^{WF}$ ser $\psi^{WF}\to\rho^{WF}$ y $(\lnot\psi)^{WF}$ ser $\lnot(\psi^{WF})$ se deduce que de las fórmulas finitas $\phi_i^{WF}$ puedes demostrar la contradicción $\psi^{WF}\land\lnot(\psi^{WF})$ .
Pero esto implica que la familia finita $\bigcup_i T_{\phi_i}$ de los axiomas de $ZF-Reg$ es inconsistente, y por lo tanto también lo es $ZF-Reg$ es decir, $CON(ZF-Reg)$ no lo hace.
Obsérvese que los dos argumentos que he esbozado no tienen nada que ver con los aspectos específicos de $ZF-Reg$ o $ZF$ . Muestran cómo, una vez que se sabe que existe un procedimiento que da el modelo de clase de una teoría, se puede concluir la implicación entre las consistencias que realmente interesaban. Por eso, muchos resultados de consistencia en la teoría de conjuntos te dicen simplemente cómo producir un modelo de clase. Entonces el mismo argumento anterior te da el resultado de consistencia real.
Hay un punto sutil que creo que debo abordar. No hay predicado de verdad para las clases propias, esto es el teorema de Tarski sobre la indefinición de la verdad. Esto significa que es no un teorema de $ZF-Reg$ que $WF$ es un modelo de $ZF$ . Más arriba, he llamado a esto un metateorema. La cuestión es que las pruebas sólo utilizan un número finito de axiomas, mientras que lo que tenemos es un procedimiento recursivo que para cada axioma $\phi$ de $ZF$ aísla un conjunto finito $T_\phi$ de los axiomas de $ZF-Reg$ que implican $\phi^{WF}$ . Pero entonces, la "prueba" real que $ZF$ tiene en $WF$ requeriría infinitos axiomas, a saber, los de $\bigcup_\phi T_\phi$ .
Esto no es tan extraño como puede parecer a primera vista. Tenga en cuenta que no hay ninguna prueba en $ZF$ que $ZF$ tiene en $V$ por la misma razón.
Por otro lado, si $M$ es un modelo de conjunto, entonces la verdad en $M$ es definible. De hecho, hay fórmulas $\phi(x,y,z)$ y $\psi(x,y,z)$ que son $\Sigma_1$ y $\Pi_1$ respectivamente, tal que (un fragmento débil de) $ZF-Reg$ son equivalentes y, para cualquier conjunto $A,B,C$ tenemos que $$\phi(A,B,C)$$ es válido si $A=(M,E)$ es una estructura en el lenguaje de la teoría de conjuntos, $B$ codifica una fórmula $\rho(\vec w)$ , $C$ es una tupla finita de elementos de $M$ (de la misma longitud que $\vec w$ y $$ (M,E)\models\rho(C).$$ Esto significa que, en contraste con la situación anterior, podemos demostrar (como un teorema de $ZF-Reg$ ) que si $M$ es un modelo de conjunto de $ZF-Reg$ entonces $WF^M$ es un modelo de $ZF$ . Esto se debe a que podemos formalizar fácilmente nuestro metateorema, una vez que podemos hablar uniformemente de la satisfabilidad de las fórmulas (que es lo que el predicado de verdad $\phi$ nos compra).
