¿Se puede derivar la imposibilidad del problema de detención del teorema de incompletitud de Godel?

Seguro. La formulación del teorema de incompletitud de Goedel dada en el enlace es “Dado cualquier conjunto de axiomas computable y consistente, hay una declaración verdadera sobre los enteros que nunca se pueden probar a partir de esos axiomas”.

Esto está redactado un poco vagamente. ¿Qué tipo de cosas cuentan como “declaraciones sobre los enteros”?

Lo que realmente significa son declaraciones de primer orden sobre aritmética de enteros; es decir, declaraciones que pueden construirse a partir de operaciones booleanas (AND, OR, NOT, …), cuantificadores (“Existe un número entero [x] tal que …”, y “Para todos los números enteros [x] es el caso que … “) Y ecuaciones polinómicas (por ejemplo,” x ^ 2 + 4y = y ^ 3 + 1 “), donde las variables en las ecuaciones polinómicas están unidas por cuantificadores.

Pero si pudiera resolver de manera computacional el Problema de detención, podría escribir fácilmente un programa (y, por lo tanto, un conjunto computable de axiomas) para determinar la verdad o la falsedad de tales declaraciones. Para determinar el estado de verdad de p Y q, primero determine recursivamente los estados de verdad de p y de q y luego combínelos en consecuencia. De manera similar para las otras operaciones booleanas. Para determinar el estado de verdad de “Existe un número entero x tal que p (x)”, primero construya recursivamente el programa que sigue corriendo a través de los números enteros y verificando el estado de verdad de p (x) con cada número entero enchufado para x, deteniéndose solo cuando esto sea cierto, compruebe si este programa se detiene alguna vez. Del mismo modo para el otro cuantificador. Finalmente, es fácil determinar el estado de verdad de una ecuación polinómica con números enchufados para cada variable (como sucederá cuando llegue a ellos).

Por lo tanto, la capacidad de resolver el problema de detención produciría la capacidad de resolver problemas arbitrarios en aritmética, por lo que el teorema de incompletitud de Goedel implica la indecidibilidad del problema de detención.

En realidad, si observa de cerca la prueba del teorema de incompletitud de Goedel, puede ver lo que hace con más detalle: establece una correspondencia entre los programas y una clase particular de fórmulas llamada [math] \ Sigma_1 [/ math] (básicamente, fórmulas que comienzan con “Existen enteros tales que …”, y todos los demás cuyos cuantificadores son de la forma “Existe un entero menor que K tal que …”) de modo que un programa se detiene si y solo si la fórmula correspondiente es verdadera , y esencialmente solo usa la prueba típica de Problema de detención para notar que esto significa que uno no puede determinar la veracidad de las declaraciones [math] \ Sigma_1 [/ math] mediante un sistema formal computable (y por lo tanto, a fortiori, no puede determinar la veracidad de declaraciones aritméticas en general por un sistema formal computable). Por supuesto, no se reconoció en estos términos cuando se escribió originalmente, pero ahora podemos reconocer esa estructura en la prueba. Con ese entendimiento, la equivalencia es obvia.

(Y si lo miras aún más de cerca, todos estos son solo modificaciones de la famosa prueba de diagonalización de Cantor, que a su vez es solo el combinador Y disfrazado, que a su vez es solo una forma de describir el proceso de arranque de un lenguaje de programación con soporte incorporado para que los programas accedan a su propio código fuente … Hay un resultado unificado que se está viendo en varias formas. Pero guardaré la explicación para más adelante. [Aquellos para quienes esto suena interesante pueden querer leer el libro de Lawvere Argumentos diagonales y categorías cerradas cartesianas “y el más accesible, pero manejable,” Un enfoque universal para las paradojas autorreferenciales “de Yanofsky])

Aquí está el argumento contrario al enlace que citó en detalles
Página en mit.edu.
Dicho esto, la diagonalización que se utiliza para demostrar que HALT es inconfundible, que es lo mismo que la prueba original de Cantor sobre las cardinalidades, que es lo mismo que las pruebas de la incompletitud de Godel y Chaitin, que son las versiones teóricas de la paradoja de Russell.
tl; dr
Tome una hoja de papel que diga en un lado “la declaración en el otro lado es falsa”, y en el otro lado “la declaración en el otro lado es verdadera”
Y eso no implica que el problema de detención sea el mismo que el de los teoremas de Godel, simplemente usan las mismas diagonalizaciones.

Un punto interesante es que estos dos resultados sustancialmente equivalentes se produjeron bastante juntos en el tiempo. Sin embargo, hasta donde se sabe, Turing y Godel no estaban al tanto del trabajo del otro, al menos hasta que ambos habían publicado.