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

Sintesi Tecnica: Auto-formalizzazione del Secondo Teorema di Incompletezza di Gödel nell'Aritmetica Ricorsiva Binaria

Definizione del Problema
Il documento riporta un esperimento di auto-formalizzazione del Secondo Teorema di Incompletezza di Gödel (Gödel II) per l'Aritmetica Ricorsiva di Base (BRA) di Church, utilizzando l'assistente alla dimostrazione Agda e il modello linguistico di grandi dimensioni (LLM) Claude. La sfida principale affrontata è la formalizzazione di un testo (le note di lezione di R. Guard del 1963) che, pur essendo preciso, contiene errori tipografici, lacune e argomenti matematici impliciti che richiedono una sostanziale ricostruzione. Un problema secondario riguarda la valutazione delle capacità e dei limiti degli attuali LLM nel generare formalizzazioni matematiche corrette da tali testi, in particolare quando le specifiche iniziali sono ambigue o errate.

Metodologia
Il progetto ha impiegato un approccio "zero-code" in cui l'autore non ha scritto alcun codice Agda; l'intero sviluppo (circa 50.000 righe) è stato generato attraverso l'interazione con Claude. La formalizzazione è stata condotta partendo da zero senza librerie esterne o tattiche, aderendo rigorosamente alle opzioni --safe --without-K --exact-split per garantire che non venissero utilizzati postulati.

La metodologia ha previsto due fasi distinte:

1. Tentativo Autonomo Iniziale: È stato effettuato un tentativo utilizzando un articolo di Rose. Questo è fallito perché il teorema sottostante nel lavoro di Rose era falso. L'LLM è riuscito a formalizzare un enunciato che somigliava superficialmente al teorema di Gödel ma era matematicamente slegato da esso, evidenziando la capacità del modello di ragionare correttamente partendo da specifiche errate.
2. Formalizzazione Corretta: Il progetto si è spostato sulle note di Guard del 1963. La formalizzazione ha richiesto la ricostruzione di argomenti impliciti, specificamente riguardo all'operazione interna di codifica dei numerali (num) e l'interazione tra sostituzione e chiusura dei numerali.
   • Framework Logico: Il sistema utilizza un calcolo in stile Hilbert con assiomi per l'uguaglianza, la logica proposizionale e la ricorsione primitiva (combinatori di Church o, u, v, C, R).
   • Internalizzazione: Un ostacolo tecnico critico è stata la mancanza di un Teorema di Deduzione nel linguaggio dell'oggetto. L'autore ha fornito a Claude la tecnica di Mario Carneiro di "sollevamento" (lifting) delle derivazioni (dimostrare P ⊃ A invece di A sotto l'ipotesi P) per gestire il ragionamento ipotetico all'interno del sistema di Hilbert.
   • Ricorsione: Il verificatore thmT (che elenca le formule derivate) è stato definito tramite ricorsione course-of-values. Poiché il ricorsore di Church R non supporta direttamente la ricorsione course-of-values standard, è stato impiegato un "trucco del R annidato" (nested-R trick) per sintetizzare un combinatore di iterazione, la cui correttezza è stata provata tramite induzione interna.
   • Sostituzione: La formalizzazione ha sostituito la complessa macchina di sostituzione simultanea multi-variabile con una sostituzione nidificata a variabile singola, facendo affidamento su un lemma di "inerzia dei numerali" (dimostrare che num(x) è chiuso sotto sostituzione) per gestire la scansione dei termini sostituiti.

Contributi Chiave e Risultati

1. Dimostrazione Verificata dalla Macchina: Il progetto ha prodotto una dimostrazione completa e verificata dalla macchina del Secondo Teorema di Incompletezza di Gödel per la BRA. Lo sviluppo contiene circa 50.000 righe di codice Agda con zero postulati.
2. Chiarificazione delle Note di Guard: La formalizzazione ha risolto esplicitamente diverse ambiguità nel testo di Guard:
   • La distinzione num vs code: Ha chiarito la differenza tra il termine interno num(x) (che calcola la codifica di un valore) e il livello meta-teorico code(x) (il handle di Gödel).
   • Lemma di Diagonale: Ha distinto tra due forme della frase di Gödel (G_sub e G_sbf) e ha colmato il divario utilizzando la sostitutività di Leibniz per i predicati.
   • Invariante di Validazione: Ha definito un comportamento canonico per il verificatore thmT su input non validi (restituendo il codice di 0=0) per garantire che le equazioni di chiusura valgano universalmente.
   • Carneiro Lift: Ha applicato sistematicamente la tecnica di sollevamento per gestire le derivazioni ipotetiche in un sistema di Hilbert privo di contesto.
3. Semplificazione Architetturale: Il progetto ha dimostrato che la sostituzione nidificata a variabile singola, combinata con il lemma di inerzia dei numerali, è sufficiente a sostituire la macchina dedicata alla sostituzione multi-variabile, riducendo il codice di circa 10.000 righe.
4. Caso di Studio LLM: Il progetto funge da caso di studio per gli LLM nella matematica. Ha dimostrato che, sebbene gli LLM possano generare prove formali complesse, possono fallire nel rilevare quando una specifica formale è matematicamente insufficiente (come visto nel tentativo con Rose) o quando una prova dipende da proprietà meta-teoriche implicite non catturate nella specifica dell'oggetto.

Significatività e Rivendicazioni
Il documento sostiene che questo esperimento suggerisce che l'uso degli LLM possa cambiare sostanzialmente l'attività di formalizzazione. Evidenzia come la teoria dei tipi sia ben adatta a rappresentare fatti combinatori sulla sintassi, permettendo la verifica della correttezza delle affermazioni. Tuttavia, nota anche i limiti: un LLM può produrre una dimostrazione "corretta" di un teorema "sbagliato" se la specifica è difettosa, mancando di una visione globale dell'intento matematico.

Il lavoro fornisce una versione completamente verificata e costruttiva del Secondo Teorema di Incompletezza di Gödel per la BRA, colmando una lacuna nella letteratura dove era precedentemente nota solo una versione per gli insiemi finiti ereditari (di Paulson). Documenta la ricostruzione degli argomenti matematici impliciti necessari per colmare il divario tra le note di lezione informali e una rigorosa dimostrazione verificata dalla macchina, offrendo un modello per futuri sforzi di auto-formalizzazione che coinvolgono testi con lacune o ambiguità. L'autore nota esplicitamente che il contenuto matematico e il testo finale sono stati revisionati dall'autore umano, mentre la generazione del codice e le sezioni specifiche (5–11) sono state generate da Claude.