Una verdad que no se puede demostrar

Desde Leibniz y Boole hasta Hilbert, distintos matemáticos imaginaron que sería posible determinar la veracidad de fórmulas matemáticas de forma automática. Nosotros ahora nos preguntamos lo mismo: hemos trabajado con sistemas lógicos sencillos que son decidibles, es decir, para los que un programa puede determinar si una fórmula es verdadera o falsa. En el caso de sistemas lógicos de más complejidad, como la aritmética de Peano, esto no es posible. Esto se debe a que la existencia de problemas computacionales indecidibles conduce directamente a la existencia de afirmaciones matemáticas no decidibles.

5.1 #Una primera aproximación

Antes de proceder a la demostración de una primera versión del Primer Teorema de Incompletitud, discutiremos de forma detallada el Programa 5.1. En la Línea 3 importamos la función es_teorema_peano, cuya existencia probamos en la Proposición 4.29. Recuerda que, como los axiomas de $\textbf{Peano}$ son recursivamente enumerables (es decir, $\textbf{Peano}$ es recursivamente axiomatizable), podemos escribir el programa es_teorema_peano(fórmula) que devuelve sí si fórmula es un teorema en $\textbf{Peano}$, y que no para en caso contrario (véase la Proposición 4.29).

import utilidades
 
from es_teorema_peano import es_teorema_peano  # NO es un oráculo
from parada_a_peano import parada_a_peano      # NO es un oráculo
 
def godel_peano(entrada):
programa_godel = utilidades.leer('godel_peano.py')
para_en_peano = parada_a_peano(programa_godel)
no_para_en_peano = 'NO (' + para_en_peano + ')'
 
if es_teorema_peano(no_para_en_peano) == 'sí':
return 'para'
else:
utilidades.ciclar()

La Línea 4 importa la función parada_a_peano, cuya existencia ya discutimos tras la Proposición 4.24. Esta función traduce, dado un programa $P$, la afirmación «$P$ para con entrada vacía» en una fórmula de $\textbf{Peano}$.

En la Línea 7 guardamos el propio programa godel_peano.py en la variable programa_godel. En la Línea 8 usamos la función parada_a_peano recién comentada, y en la Línea 9 negamos la fórmula para_en_peano. De este modo:

Ahora es cuando las cosas se ponen interesantes. Si no_para_en_peano es un teorema, la función es_teorema_peano devolverá sí, y de este modo el programa verificará la condición de la Línea 11 y devolverá para, haciendo que el programa pare. Si no_para_en_peano no es un teorema, se entrará en un bucle infinito (es_teorema_peano no parará, y por lo tanto tampoco godel_peano.py). Es claro que la Línea 14 nunca se ejecutará, pero la incluimos para enfatizar este hecho.

Ahora nos preguntamos: ¿cuál es el comportamiento de godel_peano.py con entrada vacía?

Ahora estamos en condiciones de probar el resultado principal de este trabajo.

Acabamos de demostrar que $\textbf{Peano}$ es incompleto, como ya anticipamos en la Tabla 4.1. Las consecuencias de este hecho las exploramos en detalle en la Sección 5.4. Sin embargo, paremos un momento a analizar qué es lo que acabamos de probar.

5.2 #Versión semántica

Para encontrar una fórmula verdadera y no demostrable, hemos necesitado un sistema lógico que sea, en primer lugar, recursivamente axiomatizable. Si no, no hubiésemos podido crear un programa capaz de saber cuándo una fórmula del sistema es un teorema. Por otra parte, hemos asumido que el sistema es sólido, lo cual es algo esperable. Además, necesitamos traducir efectivamente las afirmaciones sobre programas y formalizar la verificación de computaciones finitas (véase la Proposición 4.24). Reunimos estas condiciones en la siguiente definición de sistema «de tipo Turing».

No basta con que esas afirmaciones puedan escribirse en el lenguaje: necesitamos una traducción computable y que las ejecuciones finitas tengan las consecuencias demostrables indicadas. Una teoría clásica que extienda la aritmética de Robinson $Q$ permite una codificación con estas propiedades.⁴

Para entender la última condición, se puede codificar $A_P$ como «existe una computación aceptante antes de cualquier rechazo». Si $P$ acepta, una traza finita proporciona un testigo. Si rechaza tras $r$ pasos, se verifica que no aceptó antes de $r$ y que cualquier aceptación posterior tendría ya un rechazo anterior; esa misma traza permite demostrar $\neg A_P$. La capacidad de formalizar este razonamiento forma parte de la hipótesis, no se deduce de la mera consistencia.

Observemos que, sin embargo, en ningún momento hemos utilizado el sistema $\textbf{Peano}$ en sí. Esto nos indica que podríamos realizar esta demostración con otro sistema que no sea $\textbf{Peano}$, siempre y cuando verifique tales condiciones. Indicamos este resultado a continuación.

Para reforzar este importante resultado, incluimos un resumen del proceso que hemos seguido para $\textbf{Peano}$, de forma general, en la demostración de este teorema.

import utilidades
 
from es_teorema_G import es_teorema_G  # NO es un oráculo
from parada_a_G import parada_a_G      # NO es un oráculo
 
def incompleto_semantico(entrada):
programa = utilidades.leer('incompleto_semantico.py')
para_en_G = parada_a_G(programa)
no_para_en_G = 'NO (' + para_en_G + ')'
 
if es_teorema_G(no_para_en_G) == 'sí':
return 'para'
else:
utilidades.ciclar()

Nuestro resultado nos dice que, si tenemos un sistema lógico que sea recursivamente axiomatizable y de tipo Turing, no podemos esperar que pueda ser sólido y completo al mismo tiempo. Es decir, si todos los teoremas del sistema son verdaderos, siempre podremos encontrar fórmulas del sistema que sean verdaderas pero no sean teoremas.

Podemos aplicar el Teorema 5.4 a otros sistemas lógicos, siempre que verifiquen las hipótesis. Uno de ellos es, por ejemplo, el sistema de axiomas de Zermelo–Fraenkel.

5.3 #Versión sintáctica

El resultado anterior usa solidez. Ahora queremos obtener incompletitud sintáctica a partir de la hipótesis más débil de consistencia. La diferencia importa: un sistema consistente puede demostrar afirmaciones falsas sin demostrar una contradicción.

Primero necesitamos un procedimiento para decidir la demostrabilidad si, además, suponemos que el sistema es completo.

from enumera_teoremas_S import enumera_teoremas_S  # NO es un oráculo
from sintaxis_S import negar
 
def es_teorema_S(formula):
negacion_formula = negar(formula)
for teorema in enumera_teoremas_S():
if teorema == formula:
return 'sí'
if teorema == negacion_formula:
return 'no'

Ahora utilizamos la imposibilidad de resolver AdivinaConsistente mediante un predictor computable total (Proposición 3.28).⁵

from acepta_a_S import acepta_a_S  # traducción efectiva
from es_teorema_S import es_teorema_S  # bajo la suposición de completitud
 
def adivina_consistente(programa):
formula_acepta = acepta_a_S(programa)
return es_teorema_S(formula_acepta)

El caso de los programas que ciclan es esencial. No hemos supuesto que una prueba de parada implique una parada real, ni que el sistema pueda reconocer todas las ejecuciones infinitas. Consultar una prueba de parada y ejecutar después el programa podría dejar al predictor bloqueado: la consistencia por sí sola no garantiza la verdad de esa prueba. Aquí la respuesta depende únicamente de una búsqueda de demostraciones que termina por la completitud supuesta.

Hemos probado dos versiones del Primer Teorema de Incompletitud. Resumimos las diferencias entre ambas a continuación.

La formulación clásica que corresponde a este resultado es el teorema de Gödel–Rosser. Lo enunciamos a continuación con la hipótesis aritmética explícita.

Tal y como en nuestra versión sintáctica, requerimos que el sistema sea sintácticamente consistente y recursivamente axiomatizable. El teorema original de Gödel exigía como hipótesis una forma más fuerte de consistencia sintáctica llamada $\omega$-consistencia. Esta forma más general del teorema se debe al trabajo de John B. Rosser, autor del hoy conocido como truco de Rosser.⁶⁷

La tercera hipótesis exige que el sistema sea capaz de probar ciertas afirmaciones de aritmética elemental. Esto se debe a que Gödel pretendía probar que ninguna axiomatización efectiva y consistente suficientemente expresiva de la aritmética podía ser completa (véase el Capítulo 1), por lo que usó en su demostración una forma de numerar los teoremas que hoy en día se conoce como numeración de Gödel.

5.4 #Consecuencias

El Primer Teorema de Incompletitud tiene profundas implicaciones matemáticas y filosóficas.

5.4.1 #Relación con el segundo problema de Hilbert

Ya introdujimos en el Capítulo 1 los célebres problemas de Hilbert, y en concreto el segundo de ellos, que volveremos a referenciar a continuación:

1. ¿Son completas las matemáticas? Esto es, ¿puede demostrarse cada sentencia matemática o su negación?
2. ¿Son consistentes las matemáticas? Esto es, ¿no es posible probar simultáneamente una afirmación y su negación?
3. ¿Son decidibles las matemáticas? Esto es, ¿existe un método automático que pueda aplicarse a cualquier afirmación matemática, y que determine si es cierta? Este problema se conoce como el Entscheidungsproblem.

Es necesario puntualizar que la formulación de Hilbert de este problema es relativa a la aritmética. Es claro que, para tal caso, el Teorema 5.7 nos garantiza la existencia de fórmulas no demostrables, respondiendo negativamente a (1)⁸. Por otra parte, en la Proposición 4.27 probamos que la verdad en $\textbf{Peano}$ no es decidible, probando que la respuesta a la pregunta (3) es negativa. La pregunta (2) queda fuera del objeto de este trabajo.

Sin embargo, es interesante ver estas preguntas sin necesidad de limitarnos a la aritmética. Hemos introducido los sistemas lógicos justamente para poder formalizar el concepto de verdad y demostración, que son el alma de las matemáticas.

Podremos encontrar respuestas análogas para sistemas formales recursivamente enumerables y de tipo Turing. En tal caso, el Teorema 5.6 responde negativamente a la pregunta (1), mientras que una generalización de la Proposición 4.27 (similar a la que hicimos en el Teorema 5.4 a partir del Teorema 5.2) nos permite responder negativamente a la pregunta (3).

5.4.2 #Relación con la mente humana y con la tesis de Church–Turing

Algunos autores entran en conclusiones mucho más epistemológicas, y que conciernen a la mente humana. Roger Penrose y John Lucas⁹¹⁰ argumentan que el papel de la conciencia es no algorítmico cuando formamos juicios matemáticos, pudiendo generalizarlo al papel de la conciencia humana.

Para ello, los autores comentan que en cualquier sistema formal existen proposiciones indemostrables, esto es, para las que su algoritmo no puede proporcionar una respuesta. Si el funcionamiento de la mente humana fuese completamente algorítmico, entonces el algoritmo (o sistema formal) que utilice para formar sus juicios no podría tratar tal proposición. Sin embargo, la mente humana puede deducir que tal proposición es verdadera. Esta contradicción nos puede indicar que la mente humana, en cuanto al razonamiento matemático, no estaba utilizando un algoritmo en primer lugar.

Douglas Hofstadter¹¹¹² presenta los teoremas de Gödel como un ejemplo de «extraño bucle», una estructura jerárquica y autorreferencial que existe en un sistema formal. Argumenta que esta es la misma estructura que origina la conciencia, el sentido del «yo», en la mente humana: la autorreferencia proviene de la forma en que el cerebro abstrae y categoriza los estímulos en «símbolos», o grupos de neuronas, que corresponden a conceptos, en lo que es de facto un sistema formal, que eventualmente forma símbolos que corresponden a la propia entidad que realiza la percepción.

La diferencia entre las matemáticas y la conciencia reside, según Hofstadter, en el sentido en el que se realiza el razonamiento: si es «hacia arriba», desde los axiomas hacia las proposiciones y teoremas más complejas, o «hacia abajo», en el sentido contrario.

Las matemáticas funcionan hacia arriba: para derivar si una fórmula es un teorema debemos partir de los axiomas e ir razonando hasta llegar a ella. La mente humana, según el físico, funciona hacia abajo, desde un nivel más alto —de deseos, conceptos, personalidades, ideas y pensamientos— hasta el nivel más bajo de interacciones entre neuronas e incluso partículas fundamentales. Los seres humanos estamos hechos para percibir «cosas grandes» en lugar de «cosas pequeñas», incluso a pesar de que en el dominio de lo pequeño parece residir el motor de la realidad.

Ambos argumentos están íntimamente relacionados con la tesis de Church–Turing (véase la Sección 2.4). Si la mente humana es una máquina de Turing, todos los procedimientos de nuestro cerebro no serían más que algoritmos, y mediante los teoremas de Gödel, nuestra forma de razonar sería limitada —¡existen afirmaciones que no podemos demostrar!—. Esto puede inducir conclusiones más fantásticas, hablando algunos autores de que los teoremas de Gödel, aunque no permitan probarlo, son una fuerte evidencia de la existencia de dios.^{13 14}

Los ejemplos de la versión semántica están en godel_peano.py y semantic_incomplete.py, dentro de intro-to-incompleteness. Los programas de la versión sintáctica se presentan aquí como pseudocódigo actualizado; no se presupone que coincidan con los archivos de ese repositorio.