Lo que realmente dice la incompletitud

La conclusión ineludible parece ser que los matemáticos no utilizan un procedimiento de cálculo asumidamente sólido para determinar la verdad matemática. Deducimos que la comprensión matemática —el medio por el que los matemáticos llegan a sus conclusiones con respecto a la verdad matemática— no puede reducirse al cálculo ciego.

Partimos de una pregunta deliberadamente simple: ¿puede una máquina decir, de cada afirmación matemática, si es verdadera? Hilbert esperaba que la respuesta fuese sí. Tras seguir los programas y las máquinas de Turing hasta la aritmética de Peano, podemos decir algo más preciso.

Si una teoría de la aritmética es consistente, recursivamente axiomatizable y lo bastante expresiva como para hablar de la parada de programas, entonces no puede demostrar todas las afirmaciones verdaderas que es capaz de escribir. El argumento no flota en abstracto. Exhibimos un programa concreto en Python, godel_peano.py, cuyo comportamiento se traduce en una sentencia de Peano que es verdadera precisamente porque el programa no para — y esa sentencia no puede ser un teorema, o el programa acabaría parando.

La misma idea se generaliza. Cualquier sistema lógico que pueda codificar «este programa para con la entrada vacía» y enumerar sus propios teoremas hereda la incompletitud de la aritmética. La solidez (los teoremas son verdaderos) y la consistencia sintáctica (el sistema no demuestra a la vez una sentencia y su negación) dan cada una una versión del resultado. La completitud, en el sentido semántico que hemos usado a lo largo de la serie, es la víctima.

Dos distinciones hicieron la mayor parte del trabajo, y es fácil confundirlas si uno solo se encuentra la incompletitud como eslogan.

La primera es demostración frente a verdad. Una fórmula puede ser una afirmación correcta sobre los números y aun así no aparecer al final de ninguna derivación finita a partir de los axiomas. $\textbf{SumaBinaria}$ hizo concreto ese hueco con una aritmética de juguete; $\textbf{Peano}$ es el mismo fenómeno a plena potencia.

La segunda es programas frente a máquinas. Una vez que un intérprete de Python y una máquina de Turing de una sola cinta pueden simularse mutuamente, está permitido escribir las construcciones autorreferenciales en código ordinario. No es un atajo respecto al rigor: es la tesis de Church–Turing usada como licencia para elegir el modelo que los humanos pueden leer de verdad.

Nada de esto dice que las matemáticas estén rotas, ni que los ordenadores sean inútiles para demostrar teoremas. Dice que ningún paquete único de axiomas aritméticos, recursivamente axiomatizable y consistente, será jamás un procedimiento de decisión completo para las verdades de la aritmética. Si se quiere cada sentencia verdadera, no se puede exigir también un inventario mecánico de las demostraciones.

Hay una pregunta natural que no hemos respondido aquí: si un sistema así puede demostrar su propia consistencia (el segundo teorema de Gödel). Las técnicas de esta serie apuntan también a ese problema, pero pertenecen a otra historia.