Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

Resumen Técnico: Autoformalización del Segundo Teorema de Incompletitud de Gödel en la Aritmética Recursiva Binaria

Planteamiento del Problema
El artículo reporta un experimento de autoformalización del Segundo Teorema de Incompletitud de Gödel (Gödel II) para la Aritmética Recursiva Básica (BRA) de Church utilizando el asistente de pruebas Agda y el modelo de lenguaje de gran tamaño (LLM) Claude. El principal desafío abordado es la formalización de un texto (las notas de clase de 1963 de R. Guard) que, aunque preciso, contiene errores tipográficos, lagunas y argumentos matemáticos implícitos que requieren una reconstrucción sustancial. Un problema secundario consiste en evaluar las capacidades y limitaciones de los LLM actuales para generar formalizaciones matemáticas correctas a partir de tales textos, particularmente cuando las especificaciones iniciales son ambiguas o incorrectas.

Metodología
El proyecto empleó un enfoque de "código cero" donde el autor no escribió ningún código en Agda; todo el desarrollo (aproximadamente 50,000 líneas) fue generado mediante la interacción con Claude. La formalización se llevó a cabo desde cero sin librerías externas ni tácticas, adhiriéndose estrictamente a las opciones --safe --without-K --exact-split para asegurar que no se utilizaran postulados.

La metodología involucró dos fases distintas:

1. Intento Autónomo Inicial: Se realizó un intento utilizando un artículo de Rose. Este falló porque el teorema subyacente en el artículo de Rose era falso. El LLM formalizó con éxito un enunciado que se parecía superficialmente al teorema de Gödel pero que no tenía relación matemática, resaltando la capacidad del modelo para razonar correctamente a partir de especificaciones incorrectas.
2. Formalización Corregida: El proyecto se desplazó hacia las notas de 1963 de Guard. La formalización requirió la reconstrucción de argumentos implícitos, específicamente respecto a la operación interna de codificación de numerales (num) y la interacción entre la sustitución y el cierre de numerales.
   • Marco Lógico: El sistema utiliza un cálculo de estilo Hilbert con axiomas para la igualdad, lógica proposicional y recursión primitiva (combinadores de Church o, u, v, C, R).
   • Internalización: Un obstáculo técnico crítico fue la falta de un Teorema de la Deducción en el lenguaje objeto. El autor proporcionó a Claude la técnica de Mario Carneiro de "elevar" derivaciones (probar P ⊃ A en lugar de A bajo la hipótesis P) para manejar el razonamiento hipotético dentro del sistema de Hilbert.
   • Recursión: El verificador thmT (que enumera fórmulas derivadas) se definió usando recursión de curso de valores (course-of-values recursion). Dado que el recursor R de Church no soporta directamente la recursión de curso de valores estándar, se empleó un "truco de R anidado" para sintetizar un combinador de iteración, cuya corrección se probó mediante inducción interna.
   • Sustitución: La formalización reemplazó la compleja maquinaria de sustitución simultánea de múltiples variables por una sustitución anidada de una sola variable, apoyándose en un lema de "inercia de numerales" (probar que num(x) es cerrado bajo sustitución) para manejar el re-escaneo de términos sustituidos.

Contribuciones Clave y Resultados

1. Prueba Verificada por Máquina: El proyecto produjo una prueba completa y verificada por máquina del Segundo Teorema de Incompletitud de Gödel para BRA. El desarrollo contiene aproximadamente 50,000 líneas de código Agda con cero postulados.
2. Clarificación de las Notas de Guard: La formalización resolvió explícitamente varias ambigüedades en el texto de Guard:
   • La distinción num vs. code: Clarificó la diferencia entre el término interno num(x) (que computa la codificación de un valor) y el nivel meta de code(x) (el manejador de Gödel).
   • Lema de la Diagonal: Distinguió entre dos formas de la sentencia de Gödel (G_sub y G_sbf) y cerró la brecha utilizando la sustitutividad de Leibniz de predicados.
   • Invariante de Validación: Definió un comportamiento canónico para el verificador thmT sobre entradas inválidas (devolviendo el código de 0=0) para asegurar que las ecuaciones de cierre se cumplan universalmente.
   • Elevación de Carneiro: Aplicó sistemáticamente la técnica de elevación para gestionar derivaciones hipotéticas en un sistema de Hilbert libre de contexto.
3. Simplificación Arquitectónica: El proyecto demostró que la sustitución anidada de una sola variable, combinada con el lema de inercia de numerales, es suficiente para reemplazar la maquinaria de sustitución de múltiples variables, reduciendo el código base en aproximadamente 10,000 líneas.
4. Estudio de Caso de LLM: El proyecto sirve como un estudio de caso para los LLM en matemáticas. Demostró que, si bien los LLM pueden generar pruebas formales complejas, pueden fallar al detectar cuándo una especificación formal es matemáticamente insuficiente (como se vio en el intento de Rose) o cuando una prueba depende de propiedades metateóricas implícitas no capturadas en la especificación del objeto.

Significancia y Reivindicaciones
El artículo sostiene que este experimento sugiere que el uso de LLM puede cambiar sustancialmente la actividad de la formalización. Destaca que la teoría de tipos es muy adecuada para representar hechos combinatorios sobre la sintaxis, permitiendo la verificación de la corrección de las sentencias. Sin embargo, también señala las limitaciones: el LLM puede producir una prueba "correcta" de un teorema "erróneo" si la especificación es defectuosa, careciendo de una visión global de la intención matemática.

El trabajo proporciona una versión constructiva y totalmente verificada del Segundo Teorema de Incomplementud de Gödel para BRA, llenando un vacío en la literatura donde anteriormente solo se conocía una versión para conjuntos finitos hereditarios (por Paulson). Documenta la reconstrucción de los argumentos matemáticos implícitos necesarios para cerrar la bregap entre las notas de clase informales y una prueba rigurosa verificada por máquina, ofreciendo un modelo para futuros esfuerzos de autoformalización que involucren textos con lagunas o ambigüedades. El autor señala explícitamente que el contenido matemático y el texto final fueron revisados por el autor humano, mientras que la generación de código y secciones específicas (5–11) fueron generadas por Claude.