¿Por qué Turing afirma que una axiomatización completa y computable de la aritmética implicaría la decidibilidad de la lógica de primer orden?

Así que estoy leyendo el famoso artículo de Turing "Sobre números computables, con una aplicación al problema Entscheidung". Al comienzo de su prueba de la indecidibilidad de la lógica de primer orden (FOL), afirma lo siguiente:

Tal vez debería señalarse que lo que probaré es bastante diferente de los conocidos resultados de Gödel. Gödel ha demostrado que (en el formalismo de Principia Mathematica) hay proposiciones 𐌵 tales que ni 𐌵 ni ¬𐌵 son demostrables. Como consecuencia de esto, se muestra que no se puede dar ninguna prueba de consistencia de Principia Mathematica (o de K ) dentro de ese formalismo. Por otro lado, mostraré que no existe un método general que diga si una fórmula dada 𐌵 es demostrable en K o, lo que es lo mismo, si el sistema que consiste en K con ¬𐌵 adjunto como un axioma extra es consistente .

Siendo K la axiomatización de FOL dada por Hilbert y Ackermann. Además, afirma:

Si se hubiera probado la negación de lo que Gödel ha mostrado, es decir, si, para cada 𐌵 , es demostrable 𐌵 o ¬𐌵 , entonces deberíamos tener una solución inmediata del Entscheidungsproblem. Porque podemos inventar una máquina 𐌺 que probará consecutivamente todas las fórmulas comprobables. Tarde o temprano , 𐌺 llegará a 𐌵 o ¬𐌵 . Si llega a 𐌵 , entonces sabemos que 𐌵 es demostrable. Si llega a ¬𐌵 , entonces, dado que K es consistente (Hilbert y Ackermann, p. 65), sabemos que 𐌵 no es demostrable.

Entonces, de primera mano y sin mayor aclaración de su parte, parece estar equiparando dos tipos diferentes de sistemas axiomáticos formales: los que intentan mecanizar la noción de validez en lógica y los que intentan mecanizar la noción de verdad en aritmética. .

Probablemente, a lo que intenta llegar es a que hay una forma de codificar en aritmética la noción de que 𐌵 es una oración comprobable en K de modo que, si la aritmética estuviera completa, entonces esa oración podría probarse o refutarse en aritmética.

¿Alguna sugerencia para dar sentido a lo que está hablando aquí?

Gracias de antemano :)

No creo que esté equiparando nada, está haciendo una observación trivial de que todos los teoremas en un sistema axiomatizado recursivamente pueden generarse algorítmicamente. Por lo tanto, si el sistema también es completo, se obtiene un procedimiento de decisión para la demostrabilidad de cualquier oración. Porque cuando simplemente generamos todos los teoremas uno por uno, eventualmente se genera 𐌵 o ¬𐌵 y se garantiza que el procedimiento terminará.
Los sistemas axiomáticos de FOL son de naturaleza diferente a los sistemas axiomáticos para matemáticas (codificados como postulados de FOL). Tomemos un sistema axiomático de la aritmética. En aritmética, cualquier expresión sin variables libres es verdadera o falsa. Entonces, si hay un sistema completo, eventualmente aparecerá cualquier expresión en él (ya sea afirmada o negada). En una axiomatización de FOL que no es el caso, solo genera expresiones válidas y una expresión cuya negación es válida es una contradicción, no una tautología. La completitud solo implica decidibilidad en el caso de la aritmética, no en la lógica.
Esta publicación entra en más detalles sobre la diferencia entre ambos tipos de sistemas. philosophy.stackexchange.com/questions/15525/… Un sistema completo de lógica (que da salida a cada una de las expresiones válidas de esa lógica) no implica decidibilidad (ya que te dice cuándo una expresión es válida o contradictoria, pero no cuándo solo es satisfacible). Cuando digo que creo que está equiparando dos tipos diferentes de sistemas, me refiero precisamente a esta diferencia.
No creo que le importe la satisfacción. "Completitud" aquí solo significa que todo es demostrable o refutable, por lo que, por definición, implica "decidibilidad" tanto para la aritmética como para la lógica.
La integridad en un sistema lógico significa que el sistema puede generar una por una todas las expresiones válidas de la lógica. Nuevamente, la completitud en un sistema lógico no implica decidibilidad. Una expresión "simplemente satisfactoria" nunca aparecerá en las pruebas y uno no puede saberlo ya que podría ser una expresión válida que simplemente no ha aparecido todavía. De nuevo, el argumento de Turing se aplica a las axiomatizaciones de la aritmética, pero no a las axiomatizaciones de la lógica.
El artículo de Turing está escrito en 1936. Lo que ahora se entiende por completitud en un sistema lógico a diferencia de un sistema matemático es discutible, solo importa lo que él quiere decir. Y "completitud", como Turing usa la palabra, implica decidibilidad.
Los dos están fuertemente vinculados: si PA es la conjunción de axiomas de aritmética de primer orden y T es una fórmula aritmética, tenemos que PA prueba T si PA, entonces T es una fórmula válida de FO.
@MauroALLEGRANZA: Eso es falso. PA no es finitamente axiomatizable. Sin embargo, mira mi respuesta; La aritmética de Robinson (y también TC) es finitamente axiomatizable.

Respuestas (2)

Probablemente, a lo que intenta llegar es a que hay una forma de codificar en aritmética la noción de que 𐌵 es una oración comprobable en K de modo que, si la aritmética estuviera completa, entonces esa oración podría probarse o refutarse en aritmética.

Tienes toda la razón. Godel demostró (a través de su lema β) que uno puede codificar secuencias finitas de números naturales como números naturales y manipularlos, todo dentro de PA (o equivalente). Una prueba en cualquier teoría FOL computable T es simplemente una secuencia de fórmulas que satisfacen las reglas de inferencia, que obviamente pueden codificarse como una secuencia finita de números naturales. Además, si un número natural codifica o no una prueba sobre T es una oración Σ1 (es decir, de la forma "∃k (...)" donde todos los cuantificadores en "..." están acotados). Ahora PA es Σ1-completo, lo que significa que si una oración Σ1 es verdadera, entonces PA puede probarlo. Entonces, si T prueba algo, ¡PA puede probar ese hecho!

Simbólicamente, para cualquier sistema formal computable T y cualquier oración Q sobre T, si ( T ⊢ Q ) entonces ( PA ⊢ ProvT ), donde Prov[T] es un predicado en el lenguaje de PA.

Ahora debe quedar claro que el problema radica en el caso ( T ⊬ Q ); donde no tenemos garantía de que ( PA ⊢ ¬ProvT ). (Y, de hecho, Gödel demostró que, en general, no es cierto).

Pero el comentario de Turing puede fortalecerse diciendo que si hay una extensión consistente computable E de PA que prueba cada oración Σ1 verdadera y refuta cada oración Σ1 falsa, entonces podemos determinar si ( T ⊢ Q ) simplemente enunciando todos los teoremas de E hasta que encontremos una prueba o refutación de ProvT.

Su comentario original más débil es simplemente que no existe una axiomatización completa, consistente y computable de los números naturales N (es decir, un modelo de PA). Pero incluso pedir la capacidad de refutar cada oración Σ1 falsa es suficientemente malo, como se explicó anteriormente. Todo esto todavía se basa en el lema β de Gödel, pero la explicación es un poco más simple. Uno solo necesita eso ( T ⊢ Q ) iff ( N ⊨ ProvT ).

En relación con su pregunta, también me gustaría mencionar que uno puede probar directamente la indecidibilidad de FOL a través del teorema de Godel-Rosser aplicado a la aritmética RA de Robinson. RA es finitamente axiomatizable, por lo que la demostrabilidad de una oración Q sobre RA es equivalente a la demostrabilidad de una sola oración sobre FOL puro (es decir, la conjunción de los axiomas de RA implica Q). Dado que la demostrabilidad de RA es indecidible según Godel-Rosser, la demostrabilidad sobre FOL puro también es indecidible.

Si está interesado en el teorema de incompletitud de Godel-Rosser completamente generalizado, consulte esta publicación para obtener una prueba simple basada en la computabilidad.

Gracias por su cuidadosa respuesta, revisaré la publicación de blog que compartió amablemente. Solo una pregunta adicional, el último párrafo de tu explicación no me quedó del todo claro. Soy consciente de que, una vez expresadas como oraciones FOL, la demostrabilidad de una oración aritmética sería equivalente a la demostrabilidad de que una oración FOL es válida. Sin embargo, eso no descarta la posibilidad de que alguna noción de validez lógica no sea capturada dentro del modelo específico de RA. Por qué la necesidad de que sea finitamente axiomatizable.
@JavierDiego-Fernández: Lo que dices en tu segunda frase no es cierto. La demostrabilidad es siempre sobre algún sistema formal específico. No puedes simplemente decir "probable". ¿Probable sobre qué? Y parece que también tiene conceptos erróneos básicos sobre la validez lógica y los modelos. De todos modos, esto es lo que es cierto: RA está finitamente axiomatizado, por lo que tenemos ( RA ⊢ Q ) iff ( ⊢ RAX⇒Q ), donde RAX es la conjunción de los axiomas de RA. No puedes hacer esto con PA porque tiene infinitos axiomas (y no existe tal cosa como una conjunción infinita).

Probablemente, a lo que intenta llegar es a que hay una forma de codificar en aritmética la noción de que 𐌵 es una oración comprobable en K de modo que, si la aritmética estuviera completa, entonces esa oración podría probarse o refutarse en aritmética.

No creo que sea eso a lo que se refiere, en realidad. Lo que parece estar sugiriendo es que podría escribir un programa de computadora que enumere de forma recursiva todas las pruebas posibles (por ejemplo, utilizando un algoritmo de búsqueda primero en amplitud sobre el árbol de todas las pruebas posibles que podría componer a partir de los axiomas, con algunos refinamientos adicionales). para tratar con esquemas axiomáticos ). Esta es una técnica general, a la que "no le importa" cómo se ven tus axiomas. Si sabe que el sistema, sea lo que sea que codifique, es completo (que prueba cada enunciado o su negación) y consistente (que nunca prueba un enunciado y su negación), entonces esta técnica siempre encontrará una prueba o refutación de cualquier proposición. te interesa preguntar.

Sin embargo, como reconoce Turing, Gödel ya había demostrado que cualquier sistema que pueda codificar la aritmética no puede ser completo y consistente, por lo que en realidad no funciona. El argumento de Turing prueba entonces la afirmación más fuerte de que no hay ningún algoritmo que funcione en este caso.

¡Hola! Me di cuenta de tu comentario aquí y deseo responderlo, pero no quiero atraer la atención indeseable de los chiflados de allí (creo que sabes a quién me refiero). Su escepticismo es incorrecto y, presumiblemente, se debe a que en realidad no está familiarizado con la lógica matemática y ZFC. Es trivial formalizar y hacer un razonamiento sustancial sobre TM de una manera razonablemente natural (es decir, sin codificación Godel) en ACA, que es un fragmento claramente predicativo de la aritmética de segundo orden Z2, que es mucho más débil que ZFC .
En términos de fuerza, PA = ACA0 < ACA << ATR << Z2 << ZC << ZFC. Con la codificación Godel, uno puede 'hacer' un razonamiento sobre TM en PA (y en cualquier sistema que interprete PA). Así es como podemos obtener PA ⊢ Con(PA)⇒¬⬜Con(PA) donde "⬜" es el predicado de demostrabilidad. Tiene razón en que estos teoremas son simplemente argumentos de diagonalización (problemas de codificación y simulación de módulo), y es precisamente por eso que los teoremas de incompletitud de Gödel son demostrables en metasistemas tan débiles. ACA demuestra que cada subconjunto computable de N que codifica una teoría que interpreta PA− es inconsistente o incompleto.
PA solo puede probar el teorema de incompletitud para cualquier sistema formal computable específico que interprete computablemente PA− (es decir, dado un programa de computadora que es un verificador de prueba o un generador de teoremas para un sistema formal, y un programa que es una traducción de oraciones aritméticas a ese sistema que atestigua que interpreta PA−), podemos construir una prueba sobre PA de que la teoría asociada es inconsistente o incompleta), e incluso hacerlo de manera computable (es decir, podemos escribir un solo programa que, dados los programas para el sistema formal y la traducción generará la prueba deseada).
Es posible que le interesen algunos otros detalles sobre los teoremas de incompletitud en esta publicación y sobre ACA aquí . Si desea obtener más información, también es bienvenido a esta sala de chat .
¿Por qué Turing afirma que una axiomatización completa y computable de la aritmética implicaría la decidibilidad de la lógica de primer orden?
RespuestasAquíPolítica de privacidad1y, 0v