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

Resumo Técnico: Autoformalização do Segundo Teorema da Incompletude de Gödel na Aritmética Recursiva Binária

Problema
O artigo relata um experimento de autoformalização do Segundo Teorema da Incompletude de Gödel (Gödel II) para a Aritmética Recursiva Básica (BRA) de Church, utilizando o assistente de prova Agda e o modelo de linguagem de grande escala (LLM) Claude. O principal desafio abordado é a formalização de um texto (as notas de aula de R. Guard de 1963) que, embora preciso, contém erros tipográficos, lacunas e argumentos matemáticos implícitos que exigem uma reconstrução substancial. Um problema secundário envolve avaliar as capacidades e limitações dos atuais LLMs em gerar formalizações matemáticas corretas a partir de tais textos, particularmente quando as especificações iniciais são ambíguas ou incorretas.

Metodologia
O projeto empregou uma abordagem de "zero-código", onde o autor não escreveu nenhum código Agda; todo o desenvolvimento (aproximadamente 50.000 linhas) foi gerado através da interação com o Claude. A formalização foi conduzida do zero, sem bibliotecas externas ou táticas, aderindo estritamente às opções --safe --without-K --exact-split para garantir que nenhum postulado fosse utilizado.

A metodologia envolveu duas fases distintas:

1. Tentativa Autônoma Inicial: Uma tentativa foi feita utilizando um artigo de Rose. Esta falhou porque o teorema subjacente no artigo de Rose era falso. O LLM formalizou com sucesso uma afirmação que se assemelhava superficialmente ao teorema de Gödel, mas que era matematicamente não relacionada, destacando a capacidade do modelo de raciocinar corretamente a partir de especificações incorretas.
2. Formalização Corrigida: O projeto mudou para as notas de 1963 de Guard. A formalização exigiu a reconstrução de argumentos implícitos, especificamente em relação à operação interna de codificação de numerais (num) e a interação entre substituição e fechamento de numerais.
   • Estrutura Lógica: O sistema utiliza um cálculo estilo Hilbert com axiomas para igualdade, lógica proposicional e recursão primitiva (combinadores de Church o, u, v, C, R).
   • Internalização: Um obstáculo técnico crítico foi a falta de um Teorema da Dedução na linguagem do objeto. O autor forneceu ao Claude a técnica de Mario Carneiro de "elevar" derivações (provar P ⊃ A em vez de A sob a hipótese P) para lidar com o raciocínio hipotético dentro do sistema de Hilbert.
   • Recursão: O verificador thmT (que enumera fórmulas derivadas) foi definido usando recursão de curso-de-valores (course-of-values recursion). Como o recursor R de Church não suporta diretamente a recursão padrão de curso-de-valores, um "truque de R aninhado" foi empregado para sintetizar um combinador de iteração, com sua correção provada via indução interna.
   • Substituição: A formalização substituiu a complexa maquinaria de substituição simultânea de múltiplas variáveis por uma substituição aninhada de variável única, baseando-se em um lema de "inércia de numeral" (provando que num(x) é fechado sob substituição) para lidar com o re-escaneamento de termos substituídos.

Contribuições Principais e Resultados

1. Prova Verificada por Máquina: O projeto produziu uma prova completa e verificada por máquina do Segundo Teorema da Incompletude de Gödel para BRA. O desenvolvimento contém aproximadamente 50.000 linhas de código Agda com zero postulados.
2. Esclarecimento das Notas de Guard: A formalização resolveu explicitamente várias ambiguidades no texto de Guard:
   • A distinção num vs. code: Esclareceu a diferença entre o termo interno num(x) (computando a codificação de um valor) e o nível meta-teórico code(x) (o handle de Gödel).
   • Lema de Diagonalização: Diferenciou duas formas da sentença de Gödel (G_sub e G_sbf) e uniu a lacuna usando a substitutividade de Leibniz para predicados.
   • Invariante de Validação: Definiu um comportamento canônico para o verificador thmT em entradas inválidas (retornando o código de 0=0) para garantir que as equações de fechamento ocorram universalmente.
   • Elevação de Carneiro: Aplicou sistematicamente a técnica de elevação para gerenciar derivações hipotéticas em um sistema de Hilbert livre de contexto.
3. Simplificação Arquitetônica: O projeto demonstrou que a substituição de variável única aninhada, combinada com o lema de inércia de numeral, é suficiente para substituir a maquinaria dedicada de substituição de múltiplas variáveis, reduzindo o código em cerca de 10.000 linhas.
4. Estudo de Caso de LLM: O projeto serve como um estudo de caso para LLMs em matemática. Demonstrou que, embora os LLMs possam gerar provas formais complexas, eles podem falhar em detectar quando uma especificação formal é matematicamente insuficiente (como visto na tentativa de Rose) ou quando uma prova depende de propriedades meta-teóricas implícitas não capturadas pela especificação do objeto.

Significância e Alegações
O artigo alega que este experimento sugere que o uso de LLMs pode mudar substancialmente a atividade de formalização. Destaca que a teoria de tipos é bem adequada para representar fatos combinatórios sobre sintaxe, permitindo a verificação da correção de sentenças. No entanto, também nota as limitações: o LLM pode produzir uma prova "correta" de um teorema "errado" se a especificação for falha, carecendo de uma visão global da intenção matemática.

O trabalho fornece uma versão construtiva e totalmente verificada do Segundo Teorema da Incompletude de Gödel para BRA, preenchendo uma lacuna na literatura onde apenas uma versão para conjuntos finitos hereditários (por Paulson) era conhecida anteriormente. Ele documenta a reconstrução de argumentos matemáticos implícitos necessários para unir as notas de aula informais a uma prova rigorosa verificada por máquina, oferecendo um modelo para futuros esforços de autoformalização envolvendo textos com lacunas ou ambiguidades. O autor observa explicitamente que o conteúdo matemático e o texto final foram revisados pelo autor humano, enquanto a geração de código e seções específicas (5–11) foram geradas pelo Claude.