La prueba de Turing de que un oráculo de Halting es imposible y la prueba de Gödel de que una teoría aritmética de primer orden omega-consistente debe ser incompleta son similares en el sentido de que utilizan argumentos autorreferenciales. ¿Existe una relación interesante entre ellas, especialmente a la luz de la Correspondencia Curry-Howard y, sobre todo, de su versión categórica, es decir, la Correspondencia Curry-Howard-Lambek?
Respuesta
¿Demasiados anuncios?
La prueba de Turing de que un oráculo de Halting es imposible y la prueba de Gödel de que una teoría de primer orden de la aritmética omega-consistente debe ser incompleta son similares en el sentido de que utilizan argumentos autorreferenciales. ¿Existe una relación interesante entre ellas?
Bueno, el teorema de Gödel es una simple consecuencia de la prueba de Turing.
Echa un vistazo a mi Introducción a los teoremas de Gödel por ejemplo. El §43.2 (en la numeración de la segunda edición) muestra que la insolubilidad recursiva del problema de detención implica que el conjunto de verdades del lenguaje de primer orden de la aritmética no es recursivamente enumerable. Pero los teoremas en ese lenguaje de una teoría formalizada $T$ son recursivamente enumerables. Así que hay verdades que $T$ no puede probar, y si $T$ es sólida, no puede refutar tampoco. Por lo tanto, es incompleta.
§El apartado 43.3 refuerza el resultado dejando de lado la suposición de que $T$ es sólido a favor de la suposición de omega-consistencia, junto con la suposición habitual de que $T$ está axiomatizada (primitiva) recursivamente e incluye una pequeña cantidad de aritmética (por ejemplo, contiene la aritmética Q de Robinson -- lo crucial es ser lo suficientemente fuerte para representar las funciones recursivas (primitivas)). Entonces podemos demostrar que $T$ es incompleta, pasando por la irresolubilidad del Problema de Halting (es una prueba de media página en detalle, así que perdóname por no reproducirla aquí).
