Auto formalisation of Chaitin and of the surprise incompleteness Theorem

Resumen Técnico: Autoformalización de Chaitin y el Teorema de la Incompletitud Sorpresa

Problema y Contexto
Este informe extiende un experimento previo de autoformalización del segundo teorema de la incompletitud de Gödel utilizando el modelo de lenguaje de gran tamaño (LLM) Claude y el asistente de pruebas Agda. El objetivo principal es investigar las capacidades y limitaciones de los LLM actuales para formalizar pruebas matemáticas complejas, específicamente aquellas que involucran la representación interna de la computación. El documento se centra en dos objetivos específicos: la prueba de Chaitin del primer teorema de la incompletitud y la versión del teorema de la segunda incompletitud del "examen sorpresa" de Kritchman-Raz.

Un desafío técnico central abordado es la codificación de la computación dentro de la Aritmética Recursiva Básica (BRA), un sistema (formulado por Guard) que carece de cuantificadores de objeto y tácticas estándar. En tal sistema, definir una función de evaluación interna es imposible, ya que excedería los límites de la recursividad primitiva (similar a la función de Ackermann). El problema requiere representar programas y sus pasos de ejecución enteramente dentro del lenguaje objeto sin depender de funciones de meta-nivel o librerías externas.

Metodología
El proyecto emplea un enfoque "espartano" donde ningún código de Agda fue escrito por el autor humano; la formalización fue generada autónomamente por Claude basándose en descripciones matemáticas de alto nivel. La metodología se apoya en las siguientes estrategias técnicas:

1. Codificación de Cadenas Ternarias: Los programas se representan como números naturales interpretados como cadenas ternarias (dígitos 1, 2, 3). Esto permite que el conjunto de programas de longitud a lo sumo $L^*$ sea tratado como un simple segmento inicial de números naturales $\{p < N\}$, donde $N = 3^{L^*+1}$, evitando mecanismos de enumeración complejos.
2. Implementación de Máquina CK: Para evitar la necesidad de una función de evaluación global, Claude construyó autónomamente una máquina de evaluación de paso pequeño de pila de continuación (una máquina CK de Landin). Esta máquina descompone expresiones y gestiona una pila de continuaciones, permitiendo que la computación se simule paso a paso.
3. Mayoración de Gandy/Howard: Un obstáculo crítico fue probar que la máquina se detiene dentro de un número específico de pasos para una función $f$ dada dentro de la lógica. Dado que el recuento de pasos no puede ser un natural de meta-nivel, los autores guiaron a Claude para utilizar el método de mayoración de Gandy/Howard. Esto implica definir un combinador cerrado fuel(f) mediante recursión primitiva que mayoriza de manera demostrable el tiempo de ejecución real de $f$. Esto permite que la completitud del intérprete pueda enunciarse y probarse internamente dentro de BRA.
4. Examen Sorpresa como Sorites: La prueba del segundo teorema de la incompletitud evita los argumentos de conteo utilizados por Kritchman y Raz. En su lugar, modela el argumento como una paradoja de Sorites (montón de arena). El proceso procede mediante inducción externa sobre una etapa $r$, demostrando que es imposible que todos los números en el intervalo $[r, N]$ tengan descripciones cortas.

Contribuciones Clave y Resultados
El documento presenta una prueba totalmente verificada por máquina en Agda de los siguientes resultados para la Aritmética Recursiva Básica de Church:

• Teorema de Chaitin Autoformalizado: El sistema formalizó con éxito la prueba de Chaitin, que reemplaza la sentencia del mentiroso por la complejidad de Kolmogorov. La formalización produce un transformador de prueba explícito $G$. El teorema establece que si un término $w$ codifica una prueba de la sentencia de incompresibilidad $K(out(w)) > L^*$, entonces $G \cdot w$ codifica una prueba de $0=1$. Esto se formula como una implicación positiva a nivel de objeto en lugar de una negación metateórica de la demostrabilidad.
• Segunda Incompletitud Internalizada: El documento formaliza el argumento de Kritchman-Raz para mostrar que si $T$ prueba su propia consistencia ($Con_T$), entonces $T$ es inconsistente ($0=1$). La prueba procede mediante un descenso desde $S(0)$ (el principio del palomar) hacia $S(N+1)$ (una contradicción), donde cada paso $S(r) \to S(r+1)$ consume la hipótesis de consistencia exactamente una vez.
• Perspectivas Constructivas: La formalización destaca el papel de las funciones parciales en las matemáticas constructivas. Específicamente, el programa diagonal enumera las fórmulas derivables hasta que se encuentra un objetivo. Aunque el programa se demuestra que termina externamente, su tamaño se calcula sin internalizar la prueba de terminación. Esto demuestra una manifestación del fenómeno de aceleración de Blum, donde permitir un programa recursivo parcial (mantenido total por una prueba externa) permite programas de tamaño acotadamente más cortos en comparación con aquellos que deben certificar internamente su parada.

Significancia y Reivindicaciones
El documento afirma que los LLM de codificación actuales, como Claude, son herramientas efectivas para comprender los detalles granulares de los artículos matemáticos, siempre que operen bajo supervisión constante. El proyecto sirve como un estudio de caso que demuestra que:

• Los LLM pueden generar autónomamente maquinaria sintáctica compleja (parsers, máquinas de evaluación) y argumentos lógicos (mayoración) cuando son guiados por pistas estructurales de alto nivel.
• La teoría de tipos (específicamente Agda sin tácticas) es muy adecuada para expresar matemáticas concretas que involucran computación y codificación, ya que las pruebas pueden representarse directamente sin necesidad de extensionalidad de funciones o tipos cociente.
• El argumento de la "sorpresa", cuando se formaliza, se alinea más estrechamente con la paradoja de Sorites que con la tradicional paradoja del examen sorpresa, ya que la contradicción surge de la iteración de pasos válidos en lugar de un único bucle autorreferencial.

Los autores concluyen que, si bien el lenguaje de la teoría de tipos es perfecto para esta matemática computacional y combinatoria, queda una pregunta de investigación clave: cómo diseñar sistemas formales capaces de manejar objetos no combinatorios con una automatización similar. La formalización clarifica detalles implícitos en las presentaciones originales de Chaitin y Kritchman-Raz y proporciona una base rigurosa y verificada por máquina para estos argumentos dentro de un marco aritmético mínimo.