Gödel segundo teoremas de la incompletitud

Question

Generalmente Gödel del segundo teorema de la incompletitud es interpretado así: "No lo suficientemente fuerte como teoría formal puede probar su propia consistencia, suponiendo que es constante", pero en el libro Por Lindstroem "los Aspectos de la incompletitud", en el Capítulo 2 se demuestra el Teorema 7, que, según entiendo, es que a una determinada frase, que codifica la declaración de la consistencia de la teoría, todavía puede ser demostrado. Así, es esta interpretación de la segunda teorema de la incompletitud no es del todo correcto?

Decimos que $\tau^*(x)$ binumerates T en T si para cada frase $\phi$:

1. $\phi\in T\leftrightarrow T\vdash\tau^*(\phi)$
2. $\phi\not\in T\leftrightarrow T\vdash\neg\tau^*(\phi)$

Declaración de $\phi\in T$ significa que $\phi$ es el axioma de la T. $(\tau|x)(y)$ $\tau(y)\land y\le x$

Answer 1

Este es un ejemplo conocido que creo que es originalmente debido a Feferman, "Arithmetization de Metamathematics en una Configuración General", Fund. De matemáticas. 49, 1960. Para decirlo más directamente, vamos a $\tau(n)$ ser una fórmula que define el conjunto de axiomas de una coherente teoría de la $T$ ampliación de PA, y deje $\tau'(n)$ ser $$ \tau'(n) \equiv \tau(n) \de la tierra \text{Con}\{\tau(1), \ldots, \tau(n) \} $$

A continuación, $\tau'(n) \leftrightarrow \tau(n)$ mantiene para cada estándar $n$, pero $T$ no puede probar la $(\forall n)[\tau(n) \leftrightarrow \tau'(n)]$.

También, si dejamos $T'$ ser la teoría enumerados por $\tau'$ luego PA resultará $T'$ es consistente. Esto es debido a que $\tau'$ es cuidado de no incluir ningún axioma de que podría dar lugar a una incompatibilidad con los axiomas $\tau'$ ya ha aceptado por menor $n$.

La razón Feferman esta propuesta es para ilustrar el intensional carácter de la provability predicado. Dos fórmulas pueden definir de la misma teoría en el modelo estándar, mientras que no se puede probar equivalente.

Este fue previamente se le preguntó en una manera diferente en MathOverflow; véase mi respuesta allí.

Aquí hay otro ejemplo que puede ser aún más sorprendente. Deje $T$ $S$ ser eficaz teorías con $\text{PA}\vdash \text{Con}(S) \to \text{Con}(T)$ donde $\tau$ enumera la teoría de la $T$, y vamos a $$ \tau"(n) \equiv \text{Con}(S) \de la tierra \tau(n). $$ Luego, trabajando en PA, podemos razón por casos:

• Si Con(S) entonces tenemos $\text{Con}(T)$ por supuesto, y también a $(\forall n)[\tau(n) \leftrightarrow \tau''(n)]$, por lo que la teoría de la $T''$ enumerados por $\tau''$ es consistente.

• De lo contrario, si $\lnot \text{Con}(S)$, $\tau''(n)$ es idéntica falso, y así que de nuevo la teoría de la $T''$ enumerados por $\tau''$ es consistente.

Por lo tanto PA demuestra $\text{Con}(T'')$ (definido por el uso de $\tau''$) incluso si $T$ es algo así como ZFC, cuya consistencia no es demostrable en PA.

El problema, claro, es que PA no prueba en general que $(\forall n)[\tau(n) \leftrightarrow \tau''(n)]$, por lo que PA no siempre se puede decir que el $T''$ es lo mismo que $T$.