¿Encontrará esta máquina de Turing una prueba de su detención?

Question

Considere la siguiente máquina de Turing $M$ : busca sobre las pruebas ZFC válidas, en orden lexicográfico, y si encuentra una prueba que $M$ se detiene, entonces se detiene.

Si fijamos un modelo particular de máquina de Turing (digamos máquina de Turing de una sola cinta), y si fijamos un algoritmo para verificar que una cadena dada es una prueba ZFC válida del hecho de que $M$ se detiene, esto debería constituir una descripción inequívoca de una máquina de Turing $M$ .

(Los argumentos estándar de la teoría de la computabilidad, es decir, el teorema de recursión de Kleene, permiten $M$ para calcular funciones de su propia descripción).

Hace $M$ ¿Detener?

Esta pregunta me parece desconcertante porque no hay ninguna contradicción lógica aparente en ninguno de los dos sentidos. Podría haber una prueba, en cuyo caso se detendría. Si no hay prueba, entonces no se detiene. ¿De qué "depende" la respuesta? $M$ se detiene o no se detiene, pero ¿podría su comportamiento ser independiente de ZFC?

Debo señalar que una máquina de Turing estrechamente relacionada $M'$ se puede utilizar para dar una prueba sencilla del teorema de incompletitud de Godel. Es mucho más "rebelde" en su comportamiento, donde si encuentra una prueba que se detenga, no se detiene, y si encuentra una prueba que no se detenga, se detiene. De ello se deduce que no puede haber una prueba de su detención o no detención en ZFC (a menos que ZFC sea inconsistente).

Sin embargo, $M$ está tratando seriamente de averiguar su destino. ¿Cuál es?

Answer 1

Construir una segunda máquina $N$ . $N$ busca una prueba en ZFC de, "si $N$ se detiene entonces $M$ se detiene". Si encuentra uno, se detiene.

ZFC puede argumentar lo siguiente. "Supongamos $N$ se detiene. Entonces encontró una prueba de que si $N$ se detiene entonces $M$ se detiene. Esto, combinado con el rastro de $N$ que se detiene, sería una ZFC una prueba de que $M$ se detiene. Así, $M$ encuentra esto y se detiene".

Ese párrafo es una prueba ZFC de que si $N$ se detiene entonces $M$ se detiene que $N$ encuentra, así que $N$ se detiene. Por lo tanto, por la misma lógica anterior, existe una prueba de que $M$ que encontrará y se detendrá en él.

¿No es esto divertidísimo? Demostramos este hecho sobre nuestra máquina autorreferencial construyendo una segunda máquina autorreferencial. Así es como funciona básicamente la demostración del teorema de Löb (véase la respuesta de Joel David Hamkins).

Answer 2

Es una pregunta muy bonita. La respuesta es sí, la máquina encontrará una prueba de su propia naturaleza de detención, y se detendrá cuando lo haga.

Afirmo que esto es una consecuencia de Teorema de Löb . Sea $M$ ser una máquina de Turing como la que usted describe. Tenga en cuenta que no es del todo correcto decir "la" máquina de Turing que hace lo que usted dice, ya que habrá infinitas máquinas diferentes $M$ que buscan pruebas que ellos mismos detienen. Puede que inicialmente no esté claro que todos tengan el mismo comportamiento, pero permítanme mostrar que, efectivamente, todos se detienen.

Dejemos que $\psi$ sea la afirmación " $M$ se detiene". Así, podemos demostrar en ZFC que si $\psi$ es demostrable, entonces es verdadera, ya que $M$ descubriría la prueba. Por lo tanto, ZFC demuestra $\text{Pr}_{ZFC}(\ulcorner\psi\urcorner)\to\psi$ . Pero esta es exactamente la situación de la que trata el teorema de Löb, y nos dice que podemos demostrar $\psi$ directamente en ZFC. Así que podemos demostrar en ZFC que $M$ se detiene, tal y como he afirmado. De ello se deduce que podemos demostrar en PA y mucho menos que $M$ se detiene, ya que una vez que tenemos la prueba ZFC real de que se detiene, entonces podemos demostrar en una teoría muy débil que la computación real de la máquina de Turing se detiene en cualquier número específico de pasos que tomaría para verificar el hallazgo de la misma.

Ese argumento utiliza la versión ZFC del teorema de Löb, pero podemos arreglárnoslas con la versión PA estándar, aunque M está buscando pruebas en ZFC. La razón es que en PA podemos demostrar que $\text{Pr}_{PA}(\ulcorner\psi\urcorner)\to\psi$ ya que si PA demuestra que $M$ se detiene, entonces podemos demostrar que ZFC también lo hará, y así $M$ se detendrá. Por lo tanto, sólo necesitamos la versión estándar de PA del teorema de Löb para ver que PA demuestra que $M$ se detiene.

Por cierto, respecto a la versión negada y la demostración del teorema de incompletitud que mencionas al final del post, estas ideas son también la base del algoritmo universal. Véase mi artículo La lógica modal del potencialismo aritmético y el algoritmo universal .