¿Máquinas de Turing cuya terminación no es demostrable?

Tengo una pregunta ingenua: ¿existe una máquina de Turing cuya terminación sea verdadera pero no demostrable por ninguna teoría natural, consistente y finitamente axiomatizable? Pido una mera prueba de existencia en lugar de un ejemplo específico.

Esto podría tener alguna conexión con el análisis ordinal . De hecho, para una máquina de Turing , podemos definir como el menor ordinal de una teoría consistente que pruebe su terminación (o el infimum de estos ordinales). Entonces supongo que sería equivalente preguntar si existe tal que ? $M$ $O(M)$ $M$ $O(M) \geq \omega_1^{CK}$

turing-machines proof-theory halting-problem Súper 8
fuente

¿No debería la cuantificación funcionar al revés? Simplemente agregar TM X se detiene como un axioma sería consistente para cualquier X que realmente se detenga en todas las entradas (y finito si lo hace solo para el TM en cuestión). Con los cuantificadores invertidos, ¿qué tal una TM que se detiene si la entrada no es una prueba de consistencia para el sistema axiomático y de lo contrario entra en un bucle infinito?

Yonatan N

Su sugerencia es interesante, gracias. Estaba al tanto de su preocupación al formular la pregunta, es por eso que agregué "natural" en los requisitos. Por supuesto, el problema es si podemos dar una definición formal de "naturalidad" que descarte esta construcción artificial.

Super8

creo que la respuesta es no porque si se detiene, entonces uno simplemente ejecuta la máquina y se detendrá en un número finito de pasos, y eso es una prueba, y ese hecho puede convertirse en cualquier sistema de prueba razonablemente poderoso. Por otro lado, creo que es posible codificar / convertir / traducir el thm no demostrable de Godel en una máquina sin interrupción para la que no se pueda detener. esta pregunta es similar, ¿hay una TM que se detenga en todas las entradas, pero la propiedad no es demostrable cs.se

vzn

Puede construir una máquina de Turing que calcule la secuencia de Goodstein de la entrada y se detenga cuando llegue a La detención de no se puede probar en la aritmética de Peano; es decir, el Teorema de Goodstein no es demostrable usando los axiomas de Peano de la aritmética. Ver Laurie Kirby, Jeff Paris, Resultados de independencia accesibles para Aritmética de Peano (1982)

M

$M$

G (n)

$G(n)$

n

$n$

0

$0$

M

$M$

Marzio De Biasi

Gracias, no conocía esas entradas. Sin embargo, lo que pido es más fuerte, me gustaría que no se pueda probar con cualquier teoría razonable (en lugar de una teoría específica como la AP). Sin embargo, no estoy seguro de si la pregunta tiene una respuesta definitiva.

Super8

Respuestas:

La terminación de una máquina de Turing (en una entrada fija) es una oración y todas las teorías aritméticas de primer orden usuales están completas para las oraciones , es decir, todas las declaraciones verdaderas son demostrables en estas teorías. $\Sigma^0_1$ $\Sigma^0_1$ $\Sigma^0_1$

Si observa la totalidad en lugar de detenerse , es decir, un TM se detiene en todas las entradas, entonces esa es una oración y para cualquier teoría coherente axiomatizable computable que sea lo suficientemente fuerte (por ejemplo, se extiende, por ejemplo, teoría de Robinson ) existe Una TM cuya totalidad no puede ser probada en esa teoría. $\Pi^0_2$ $Q$

Kaveh
fuente

Sí, estaba buscando la totalidad, ya que, por supuesto, el problema es trivial para una entrada fija. Pensaré en su reclamo y en cómo probarlo, pero en este punto no veo cómo considerar las teorías "computablemente axiomatizables" descarta el problema antes mencionado. Además, en su declaración, el TM depende de la teoría considerada, ¿podemos obtener mi declaración más fuerte mediante algún tipo de diagonalización?

Super8

Aquí hay una manera fácil: el conjunto de funciones computables probables totales de tal teoría es ce, el conjunto de funciones computables totales no es ce, o alternativamente puede diagonalizar contra las funciones probables totales de la teoría.

Kaveh

Pensándolo bien, sugiero considerar una restricción del problema de la siguiente manera. Dado un sistema de notación ordinal representa un ordinal , podemos definir una "teoría elemental" correspondiente que permite la inducción transfinita hasta . Dada una TM , entonces definiríamos como el ordinal más pequeño de modo que la terminación de pueda ser probada por una teoría (es decir, el sistema de notación puede ser libremente elegido). ¿Tiene sentido esta definición?

σ

$\sigma$

α

$\alpha$

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$

α

$\alpha$

M

$M$

O (M)

$O(M)$

α

$\alpha$

M

$M$

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$

Super8

@ Super8, no estoy seguro. En general, la asociación de ordinales a teorías no es canónica, hay varias formas de asociarse para hacerlo. Puede comenzar con una teoría débil como PRA y agregar inducción sobre ordinales computables con buenas secuencias fundamentales, etc. pero no estoy seguro de por qué le gustaría hacerlo.

Kaveh

Ok, no me había dado cuenta del problema, entonces intentaré encontrar una mejor definición por mi cuenta.

Super8

No soy un experto en lógica, pero creo que la respuesta es no . Si la máquina de Turing se detiene, y el sistema es lo suficientemente fuerte, debería poder escribir el historial de cómputo completo de la máquina de Turing en su entrada. Cuando uno verifica que el resultado del cálculo es una secuencia final de transiciones, se puede ver que la máquina se detiene. Independientemente de cómo formalice las máquinas de Turing en su teoría, debería poder demostrar en cualquier teoría razonable que una máquina que se detiene realmente se detiene. A modo de analogía, piense en tratar de demostrar que una suma finita es igual a lo que es igual; por ejemplo, demuestre que 5 + 2 + 3 + 19 + 7 + 6 = 42, o 5 + 5 + 5 = 15. Así como esto siempre es posible, siempre y cuando el número de pasos sea finito, también lo está demostrando el resultado de un cálculo finito.

Solo como un punto obvio adicional: incluso si su teoría es inconsistente, aún puede demostrar que la máquina se detiene, incluso si no lo hace, ya que puede probar cualquier wff en una teoría inconsistente, independientemente de si es o no En realidad cierto.

Philip White
fuente

Estoy de acuerdo con su primer punto, vea mi respuesta a continuación. Con respecto a su segundo punto, una teoría inconsistente también probará la terminación de un TM (en realidad no determinante), de ahí la restricción a teorías consistentes.

Super8

Creo que estamos diciendo lo mismo; Me acabo de dar cuenta de que dijiste "coherente" en la pregunta, perdón por perderte eso. Creo que la respuesta de Kaveh cubre las mismas cosas y, de todos modos, está escrita con más elegancia.

Philip White