Es simplemente una reformulación del teorema de Gödel : si usted tiene cierta intuición para el teorema de Gödel, a continuación, usted puede transferir el teorema de Löb.
De hecho, si PA demuestra $Prov(A)\to A$ significa que el provability de $A$ es suficiente para concluir la verdad de la $A$ : pero sabemos que algunos modelos pueden creer que algunas cosas son demostrables, mientras que no : este es el teorema de Gödel con $A= "0=1"$.
Así que si $Prov(A)\to A$ es comprobable que significa que cualquier modelo que piensa que tiene una prueba de $A$ no es malo acerca de esto : esto sólo puede suceder si $A$ es cierto.
Para ver con mayor precisión por qué es tan sólo del teorema de Gödel : supongamos que usted tiene un $A$, y asumir la $T=$PA + $\neg A$ es consistente. En particular, $T$ es una constante recursivamente axiomatizable extensión de la PA, así que no puede probar su propia consistencia (Gödel); en particular, no es $\varphi$ tal que $T\vdash \neg Prov_T(\varphi)$.
Sin embargo, $PA\vdash Prov_{PA}(A)\to A$ $T\vdash \neg Prov_{PA}(A)$ por lo tanto $T\vdash \neg Prov_T(0=1)$$T\vdash Con(T)$ : una contradicción.
Por el contrario, el teorema de Löb puede ser usado para demostrar el teorema de Gödel para PA: si PA es consistente, entonces PA$\nvdash 0=1$, por lo que por Löb PA$\nvdash Prov_{PA}(0=1) \to (0=1)$ por lo tanto PA $\nvdash \neg Prov_{PA}(0=1)$: PA no probar su propia consistencia (por supuesto, esto funciona para cualquier niza $T$ ampliar PA)
Apéndice : yo he reducido "de la intuición por el teorema de Löb" a "de la intuición por el teorema de Gödel", pero aún no han dado el último. Para este caso es "simplemente" que una teoría satisfactoria de las hipótesis que se puede hablar de sí mismo y de sus pruebas y por lo tanto puede, en efecto, reproducir la paradoja del mentiroso : hay una frase que representa "yo no soy demostrable"
