Auto formalisation of Chaitin and of the surprise incompleteness Theorem

Resumo Técnico: Autoformalização de Chaitin e o Teorema da Incompletude Surpresa

Problema e Contexto
Este relatório estende um experimento anterior de autoformalização do segundo teorema da incompletude de Gödel utilizando o modelo de linguagem de grande escala (LLM) Claude e o assistente de prova Agda. O objetivo primário é investigar as capacidades e limitações dos LLMs atuais na formalização de provas matemáticas complexas, especificamente aquelas que envolvem a representação interna de computação. O artigo foca em dois alvos específicos: a prova de Chaitin para o primeiro teorema da incompletude e a versão do teorema da incompletude segundo de Kritchman-Raz, baseada no "paradoxo do exame surpresa".

Um desafio técnico central abordado é a codificação de computação dentro da Aritmética Recursiva Básica (BRA), um sistema (formulado por Guard) que carece de quantificadores de objeto e táticas padrão. Em tal sistema, definir uma função de avaliação interna é impossível, pois excederia os limites recursivos primitivos (semelhante à função de Ackermann). O problema exige a representação de programas e seus passos de execução inteiramente dentro da linguagem de objeto, sem depender de funções de meta-nível ou bibliotecas externas.

Metodologia
O projeto emprega uma abordagem "espartana", onde nenhuma linha de código Agda foi escrita pelo autor humano; a formalização foi gerada autonomamente pelo Claude com base em descrições matemáticas de alto nível. A metodologia baseia-se nas seguintes estratégias técnicas:

1. Codificação de String Ternária: Os programas são representados como números naturais interpretados como strings ternárias (dígitos 1, 2, 3). Isso permite que o conjunto de programas de comprimento no máximo $L^*$ seja tratado como um simples segmento inicial de números naturais $\{p < N\}$, onde $N = 3^{L^*+1}$, evitando mecanismos de enumeração complexos.
2. Implementação da Máquina CK: Para contornar a necessidade de uma função de avaliação global, o Claude construiu autonomamente uma máquina de avaliação de passo pequeno de pilha de continuação (uma máquina CK de Landin). Esta máquina decompõe expressões e gerencia uma pilha de continuações, permitindo que a computação seja simulada passo a passo.
3. Majoração de Gandy/Howard: Um obstáculo crítico foi provar que a máquina para dentro de um número específico de passos para uma determinada função $f$ dentro da lógica. Como a contagem de passos não pode ser um natural de meta-nível, os autores guiaram o Claude para usar o método de majoração de Gandy/Howard. Isso envolve a definição de um combinador fechado fuel(f) via recursão primitiva que majora comprovadamente o tempo de execução real de $f$. Isso permite que a completude do intérprete seja enunciada e provada internamente na BRA.
4. Surpresa como Sorites: A prova do segundo teorema da incompletude evita os argumentos de contagem usados por Kritchman e Raz. Em vez disso, o artigo modela o argumento como um paradoxo de Sorites (amontoado de areia). O processo procede por indução externa em um estágio $r$, provando que é impossível que todos os números no intervalo $[r, N]$ possuam descrições curtas.

Principais Contribuições e Resultados
O artigo apresenta uma prova totalmente verificada por máquina em Agda dos seguintes resultados para a Aritmética Recursiva Básica de Church:

• Teorema de Chaitin Autoformalizado: O sistema formalizou com sucesso a prova de Chaitin, que substitui a sentença do mentiroso pela complexidade de Kolmogorov. A formalização produz um transformador de prova explícito $G$. O teorema afirma que, se um termo $w$ codifica uma prova da afirmação de incompressibilidade $K(out(w)) > L^*$, então $G \cdot w$ codifica uma prova de $0=1$. Isso é formulado como uma implicação positiva de nível de objeto, em vez de uma negação meta-teórica de provabilidade.
• Segunda Incompletude Internalizada: O artigo formaliza o argumento de Kritchman-Raz para mostrar que, se $T$ prova sua própria consistência ($Con_T$), então $T$ é inconsistente ($0=1$). A prova procede por um descenso de $S(0)$ (o princípio da casa do pombo) para $S(N+1)$ (uma contradição), onde cada passo $S(r) \to S(r+1)$ consome a hipótese de consistência exatamente uma vez.
• Insights Construtivos: A formalização destaca o papel das funções parciais na matemática construtiva. Especificamente, o programa diagonal enumera fórmulas deriváveis até que um alvo seja encontrado. Embora o programa seja provado como terminante externamente, seu tamanho é calculado sem internalizar a prova de terminação. Isso demonstra uma manifestação do fenômeno de aceleração de Blum, onde permitir um programa recursivo parcial (mantido total por uma prova externa) permite programas desproporcionalmente mais curtos do que aqueles que devem certificar a terminação internamente.

Significância e Alegações
O artigo alega que os atuais LLMs de codificação, como o Claude, são ferramentas eficazes para compreender os detalhes granulares de artigos matemáticos, desde que operem sob supervisão constante. O projeto serve como um estudo de caso demonstrando que:

• LLMs podem gerar autonomamente maquinaria sintática complexa (parsers, máquinas de avaliação) e argumentos lógicos (majoração) quando guiados por pistas estruturais de alto nível.
• A teoria de tipos (especificamente Agda sem táticas) é bem adequada para expressar matemática combinatória concreta envolvendo computação e codificação, pois as provas podem ser representadas diretamente sem a necessidade de extensionalidade de funções ou tipos de quociente.
• O argumento da "surpresa", quando formalizado, alinha-se mais proximamente ao paradoxo de Sorites do que ao tradicional paradoxo do exame surpresa, já que a contradição surge da iteração de passos válidos em vez de um único loop autorreferencial.

Os autores concluem que, embora a linguagem da teoria de tipos seja perfeita para esta matemática computacional e combinatória, uma questão de pesquisa fundamental permanece: como projetar sistemas formais capazes de lidar com objetos não combinatórios com automação semelhante. A formalização esclarece detalhes implícitos nas apresentações originais de Chaitin e Kritchman-Raz e fornece uma base rigorosa e verificada por máquina para esses argumentos dentro de um arcabouço aritmético mínimo.