¿Qué hay de malo con esta prueba de ZF ser incompatible?

Question

Estoy estudiando (de forma independiente) de la lógica matemática y en la investigación de auto-referencial declaraciones que he desarrollado un resultado que no sé cómo interpretar. Voy a usar la notación de Enderton "Un matemáticas introducción a la lógica" (p 266-267):

Deje $T$ ser cualquier suficientemente fuerte recursivamente axiomizable teoría (PA o ZF) y deje $\sf Prb_T \sigma$ (Aquí se $\sf Prb_T$ abrevia "comprobable en $T$") expresa que $\sigma$ tiene una deductivo prueba en $T$. (es decir,$\sf Prb_T \sigma$$T \vdash \sigma$). Vamos $\sf Cons T$ ser una frase expresando que $T$ es consistente (como $\neg \sf Prb_T (0=1))$. A continuación, utilizando el punto fijo lema que podemos llegar a una sentencia de $\sigma$ tal forma que:

$$T \vdash (\sigma \leftrightarrow \sf Prb_T (\sf Contras T \rightarrow \neg \sf Prb_T \sigma))$$

Ahora bien $T \vdash \sigma$ o $T \nvdash \sigma$. Voy a demostrar que no podemos tener ya sea asumiendo $T$ es consistente.

Si $T \vdash \sigma$, según nuestra definición de $\sigma$ tenemos que $T \vdash \sf Prb_T (\sf Cons T \rightarrow \neg \sf Prb_T \sigma)$. Esto implica que $T \vdash (\sf Cons T \rightarrow \neg \sf Prb_T \sigma)$ Pero esto significa que tenemos una prueba de $T$ siendo coherente implica $T \nvdash \sigma$ que esto contradice la hipótesis inicial de $T \vdash \sigma$. Por lo tanto, asumiendo $T$ es consistente, debemos tener $T \nvdash \sigma$. Pero este también conduce a una contradicción, por la construcción de la $\sigma$ ahora tenemos $T \nvdash \sf Prb_T (\sf Contras T \rightarrow \neg \sf Prb_T \sigma)$. This means that there is no proof of $T$ se en consonancia con lo que implica que $T \nvdash \sigma$. Sin embargo, acabamos de proporciona una prueba (aunque meta-matemáticos en la naturaleza), como testimonio este hecho.

Entonces, ¿qué debo lógicamente concluir de esto? Me imagino que este implica que $T$ es inconsistente. Supongo que no hay otra posibilidad: la de Que todo este resultado y la prueba no puede ser formalizado por lo tanto la eliminación de la contradicción (o tal vez no, porque entonces podríamos tener una contradicción con el Teorema de Completitud de la lógica de primer orden). Yo sé que por Gödel Segundo Teorema de la Incompletitud asumiendo $T$ es consistente, a continuación,$T \nvdash \sf Cons T$. Sin embargo $T$ todavía puede probar algunos hechos acerca de las implicaciones que involucran $\sf Cons T$ (De hecho, Enderton da un ejemplo en la parte inferior de la página 267). Mi entendimiento es que la mayoría de los meta-matemático de los resultados de tales como teorema de la incompletitud de Gödel y Tarski del teorema de undefinability puede ser representado y probado en el cálculo deductivo. Estoy equivocado en este? Si no estoy, a continuación, lo que hace que este resultado diferente?

Answer 1

El problema con el argumento, de hecho, con la mayoría de las reclamaciones de este tipo es que la internalización de la lógica y las pruebas son sólo tan bueno como su estándar de los números enteros, sino que se vuelven incontrolables cuando nos movemos hacia adelante de ellos.

¿A qué me refiero con eso? Sabemos que cada real, meta-teórica, la prueba corresponde a un determinado número natural. Y sabemos que $T$ sí tiene un predicado que se interpreta como exactamente los códigos de los axiomas de la $T$.

Pero esto sólo sucede en los modelos donde los enteros son estándar. Si usted no estándar enteros, invariablemente agregar nuevos axiomas a $T$ y agregar nuevas reglas de inferencia de la lógica, y por lo que añadió nuevas maneras de probar que $0=1$.

Así que la forma de reconciliar esta es notar que, de hecho, un modelo de $\sf ZFC+\lnot\operatorname{Con}(ZFC)$ no debe estar de acuerdo con su meta-teoría acerca de los números enteros (es decir, se debe tener no estándar enteros que será testigo de este).