Ver el Teorema de Löb, por ejemplo en :
Supongamos que se produce una demostrable de punto fijo para la propiedad de ser un teorema de $\mathsf {PA}$, en lugar de (como en la prueba de Gödel) la propiedad de no ser teorema de $\mathsf {PA}$. En otras palabras, vamos a $H$ (de Leon Henkin, el primero que planteó esta cuestión) ser una aritmética declaración de la formalización "esta declaración es comprobable en $\mathsf {PA}$." Es $H$ comprobable en $\mathsf {PA}$ o no ? Reflexionar sobre el significado de $H$ sólo los rendimientos que $H$ es verdadera si y sólo si es comprobable en $\mathsf {PA}$, lo cual no nos lleva a ninguna parte, y que en un principio podría parecer desesperada para decidir si este extraño auto-referencial frase es comprobable en $\mathsf {PA}$ o no.
Löb resuelto el problema de la provability de $H$, demostrando que tiene más general, que si $\mathsf {PA}$ demuestra "si $\mathsf {PA}$ demuestra $A$$A$", $\mathsf {PA}$ demuestra $A$ [mi además : si $\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$,$\mathsf {PA} \vdash A$] (de modo que, en particular, la Henkin frase es comprobable en $\mathsf {PA}$).
Para ver esto, considere la posibilidad de la teoría de la $\mathsf {PA} + \lnot A$. Estamos suponiendo que la $\mathsf {PA}$ demuestra "si $\mathsf {PA}$ demuestra $A$$A$," lo que implica "si $\lnot A$ $\mathsf {PA}$ no demuestran $A$." Pero esto a su vez implica la "si $\lnot A$ $\mathsf {PA} + \lnot A$ es consistente," por lo $\mathsf {PA} + \lnot A$ demuestra la consistencia de $\mathsf {PA} + \lnot A$, y por lo tanto es de hecho incompatible, lo que implica que $\mathsf {PA}$ demuestra $A$. El mismo argumento se aplica a cualquier teoría de la $T$ por el cual el segundo teorema de la incompletitud de las suspensiones.
El segundo teorema de la incompletitud es un caso especial del teorema de Löb, como vemos por la elección de $A$ en la formulación del teorema como una contradicción lógica "$B$$\lnot B$." Para tal $A$, "$\mathsf {PA}$ prueba $A$" es lo mismo que decir "$\mathsf {PA}$ es inconsistente," y cualquier hipotética declaración de la "si $C$ $A$" es lógicamente equivalente a $\lnot C$. Por lo tanto, del teorema de Löb nos dice que si $\mathsf {PA}$ demuestra "$\mathsf {PA}$ no es incompatible", a continuación, $\mathsf {PA}$ es incoherente, o en otras palabras, si $\mathsf {PA}$ es consistente, a continuación, $\mathsf {PA}$ no demostrar "$\mathsf {PA}$ es consistente."
Löb del teorema nos da una bastante extraño principio para la demostración de teoremas acerca de los números naturales. Con el fin de demostrar $A$, es admisible asumir como premisa que el $A$ es comprobable en $\mathsf {PA}$, mientras que el argumento es uno que puede ser formalizado en el $\mathsf {PA}$. Porque si hay una prueba en $\mathsf {PA}$ "si hay una prueba de
en $\mathsf {PA}$ $A$ $A$ " entonces no es una prueba en $\mathsf {PA}$$A$. Un principio similar se mantiene, por ejemplo, para $\mathsf {ZFC}$. Este principio no tiene ninguna aplicación conocida en probar todos los teoremas matemáticos acerca de los números primos o
otros asuntos de la matemática tradicional de interés, pero tiene usos en la lógica.
Löb principio puede parecer desconcertante en lugar de simplemente extraño. ¿Cómo puede ser admisible, en la comprobación de $A$, asumir que $A$ es comprobable en $\mathsf {PA}$? Después de todo, lo que es comprobable en $\mathsf {PA}$ es verdadera, por lo que no podemos concluir sin más preámbulos que $A$ es cierto, y lo demuestran $A$ sin hacer ningún razonamiento? El punto esencial aquí es que es admisible suponer que $A$ es comprobable en $\mathsf {PA}$ cuando se acredite $A$ sólo si el razonamiento que conduce desde la suposición de que $A$ es comprobable en $\mathsf {PA}$ a la conclusión de $A$, de hecho, puede ser llevado a cabo dentro de $\mathsf {PA}$. Que todo lo comprobable en $\mathsf {PA}$ es cierto no es algo que pueda ser establecido dentro de $\mathsf {PA}$ sí, como se muestra por el segundo teorema de la incompletitud. Decir que, por ejemplo, $0 = 1$ es verdadera si comprobable en $\mathsf {PA}$ ($0$ no es igual a $1$) lo mismo que decir que $0 = 1$ no es comprobable en $\mathsf {PA}$, o en otras palabras, que el $\mathsf {PA}$ es consistente.
Podemos "formalizar" Franzén argumento :
1) asumir : $\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$
2) $\mathsf {PA} \vdash \lnot A \to \lnot \rm Pr_\mathsf{PA}(\ulcorner A \urcorner)$ --- a partir de 1) por implicación tautológica
3) $\mathsf {PA} \vdash \lnot A \to \rm Cons (\mathsf{PA} + \lnot A)$
4) $\mathsf {PA} + \lnot A \vdash \rm Cons (\mathsf{PA} + \lnot A)$ --- contradicción
5) $\mathsf {PA} \vdash A$ --- de 4) por Reductio Ad Absurdum.
Por supuesto, de la tautología : $\varphi \to (\psi \to \varphi)$ hemos : si $\mathsf {PA} \vdash A$,$\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$; por lo tanto, concluimos con :
$\mathsf {PA} \vdash A \ \ $ fib $ \ \ \mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$.
Ver : George Boolos & John Burgess & Richard Jeffrey, Computabilidad y la Lógica (5ª ed - 2007), corolario del teorema de Löb, página 237 :
Corolario 18.5 : Supongamos que $\rm Pr_T(x)$ es un provability predicado por $T$. Entonces si $T \vdash H ↔ \rm Pr_T(\ulcorner H \urcorner)$,$T \vdash H$.
Prueba: Inmediata a partir del teorema de Löb.
La conclusión siguiente de BBJ el Corolario es :
la sentencia de $H$ afirmar de sí mismo que es "demostrable" ($H ↔ \rm Pr_\mathsf{PA}(\ulcorner H \urcorner)$) es demostrable, y por lo tanto es cierto y demostrable.
Por el Corolario anterior : si $T \vdash H ↔ \rm Pr_T(\ulcorner H \urcorner)$,$T \vdash H$. Pero $H ↔ \rm Pr_T(\ulcorner H \urcorner)$ y por lo tanto, la sustitución de $\rm Pr_T(\ulcorner H \urcorner)$ $H$ en la premisa, tenemos $T \vdash H ↔ H$, que es una tautología.
Por lo tanto, concluimos con $T \vdash H$ (bajo ninguna hipótesis) : $H$ es demostrable y por lo tanto, la afirmación de su propia provability, es cierto. I. e. : es cierto y demostrable.
De acuerdo con la discusión anterior, podemos volver a Odifreddi de la reclamación.
El contexto [véase página 169] es explícitamente que de Löb del teorema :
Volviendo a la auto-referencia, hemos visto que la sentencia de la afirmación de su propia
unprovability es cierto y no demostrable. Ahora queremos demostrar que, en las
condiciones antes mencionadas [los tres Löb propiedades de $\rm Pr_T$], la sentencia de la afirmación de su propia provability es cierto y demostrable. Esto proporciona un ejemplo de la verdadera auto-referencial declaración que no hace uso de la negación. El resultado general es que, en las condiciones indicadas anteriormente, una frase $\psi(\overline x) \to \psi_x$ (afirmando que si $\psi_x$ es demostrable, entonces es verdadero, y por lo tanto expresan una forma de solidez) es comprobable si y sólo si $\psi_x$ es (Teorema de Löb). [...]
Puesto que la fórmula que afirma su propia provability tiene la propiedad de que $\vdash_\mathcal F \psi(\overline x) \leftrightarrow \psi_x$, en particular, que $\psi(\overline x) \to \psi_x$ es demostrable, y lo es $\psi_x$ sí, por el Teorema de Löb.
Hasta ahora, "todo funciona" ...
Un ejemplo similar, basándose en las mismas condiciones en el provability predicado, pero no el uso de Gödel del Segundo Teorema, es la sentencia de la afirmación de sí mismo, que si es demostrable, entonces es verdadera, es decir,$\vdash_\mathcal F \psi(\overline x) \leftrightarrow (\psi(\overline x) \to \psi_x)$.
Supongamos $\psi_x$ es demostrable. A continuación, $\vdash_\mathcal F \psi(\overline x)$ por la representabilidad de provability, y $\vdash_\mathcal F (\psi(\overline x) \to \psi_x)$, por definición, de $\psi_x$. Por modus ponens, $\vdash_\mathcal F \psi_x$. Así tenemos
demostró que si $\psi_x$ es comprobable, es decir, si $\psi(\overline x)$ se mantiene, entonces para qué $\psi_x$. Esta establece que si $\psi_x$ es demostrable, entonces es verdadero. Por $\psi_x$ afirma exactamente esto, y por lo tanto es cierto y demostrable.
Se trata de una versión de "Henkin de la paradoja", con Comprobable en lugar de True ; véase MH Lob, la Solución de un Problema de Leon Henkin (1955).
Voy a tratar de "descansar" el argumento anterior.
Mi primera afirmación es que Odifreddi "casual"referencia a "un ejemplo [...] no es el uso de Gödel del Segundo Teorema" debe ser interpretado como que apunta a una "semántica" argumento.
Voy a usar las $O$ para Odifreddi de la sentencia; por lo tanto, Odifreddi afirma que :
la sentencia de $O$ afirmar de sí mismo que "si es demostrable, entonces es verdadero" es demostrable, y por lo tanto es cierto y demostrable.
Suponga que $O$ es comprobable en $\mathsf{PA}$. A continuación, utilizando la prueba de predicado para expresar este hecho, tenemos que $\rm Pr_\mathsf{PA}(\ulcorner O \urcorner)$ es verdadero.
Si $\mathsf{PA}$ es de sonido, a continuación, $\rm Pr_\mathsf{PA}(\ulcorner O \urcorner) \to O$ debe ser verdadera (esto es, en general, para cualquier frase, $S$ en lugar de $O$), y así, por modus ponens, tenemos que $O$ es verdadero.
Por lo tanto, suponiendo que la solidez de $\mathsf{PA}$ , $O$ es verdadero.
Ahora, parafraseando a Odifreddi :
Esta establece que si $O$ es demostrable, entonces es verdadero.
Podemos "formalizar" la prueba en $\mathsf{PA}$, y por lo tanto :
$\mathsf{PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner O \urcorner) \to O$.
La aplicación del teorema de Löb, se concluye con :
$\mathsf{PA} \vdash O$.
Odifreddi de nuevo :
Pero $O$ afirma exactamente esto, y por lo tanto es cierto y demostrable.
