Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Sintesi Tecnica: Unificazione dei Sistemi Sequent per la Logica della Provabilità di Gödel-Löb

Problema
Il saggio affronta una lacuna significativa nella teoria della dimostrazione della logica della provabilità di Gödel-Löb (GL). Sebbene GL possieda una ricca varietà di formalismi di tipo sequent senza taglio, le relazioni tra di essi non erano state pienamente stabilite. Nello specifico, il lavoro precedente aveva stabilito corrispondenze proof-teoretiche tra:

1. Sistemi strutturali: il sistema di sequenti etichettati di Negri ($G3KGL$) e il sistema di tree-ipersequenti di Poggiolesi ($CSGL^*$), tramite Goré e Ramanayake.
2. Generalizzazioni della struttura della prova: il sistema di Gentzen di Sambin e Valentini ($GL_{seq}$), il sistema non ben fondato di Shamkanov ($GL_\infty$) e il sistema ciclico di Shamkanov ($GL_{circ}$), tramite Shamkanov.

Tuttavia, l'inter-traslatabilità delle prove tra i sistemi strutturali ($G3KGL$, $CSGL^*$) e le generalizzazioni della struttura della prova ($GL_{seq}$, $GL_\infty$, $GL_{circ}$) rimaneva un problema aperto. La difficoltà intrinseca risiede nel trasformare le prove che utilizzano complessi sequenti strutturali (grafi o alberi di sequenti di Gentzen) in prove che utilizzano standard sequenti di Gentzen, un processo che richiede lo "spogliamento" di questi dati strutturali extra.

Metodologia
L'autore, Tim S. Lyon, risolve questo problema aperto costruendo una catena di trasformazioni sintattiche delle prove che colma il divario tra questi distinti formalismi. La metodologia procede in tre fasi primarie:

1. Ristrutturazione in forma end-active: Il saggio dimostra prima come ristrutturare le prove nel sistema di tree-ipersequenti $CSGL^*$ in una forma "end-active". In una prova end-active, le formule principali e ausiliarie delle regole di inferenza compaiono solo nelle (pre-)foglie della struttura del tree-sequent. Ciò si ottiene permutando le regole non end-active verso il basso attraverso l'albero della prova, sfruttando l'invertibilità preservante l'altezza delle regole in $CSGL^*$.

2. Linearizzazione: Viene introdotta una nuova "tecnica di linearizzazione" per trasformare queste prove di tree-sequent end-active in prove che utilizzano sequenti annidati lineari. Questa tecnica consiste nell'identificare percorsi specifici dalla radice a una foglia nel tree-sequent e nel "potare" i sotto-alberi, efficacemente collassando la struttura ad albero in una sequenza lineare di sequenti di Gentzen. Questo processo genera un nuovo calcolo, LNGL (Calcolo per Sequenti Annidati Lineari per GL).

3. Forma Normale e Traduzione in Gentzen: Il saggio mostra che le prove in LNGL possono essere trasformate in una specifica forma normale. In questa forma, le prove procedono in stadi ripetitivi: regole locali, seguite da regole di propagazione ($4L$ e $\Box L$), e infine la regola modale ($\Box R$). Questa prova strutturata è poi tradotta nel sistema di Gentzen di Sambin e Valentini ($GL_{seq}$). Infine, trasformazioni standard mappano le prove in $GL_{seq}$ nuovamente verso il sistema etichettato $G3KGL$ e verso i sistemi ciclici/non ben fondati ($GL_{circ}$, $GL_\infty$).

Contributi Chiave

• Nuovo Calcolo (LNGL): Il saggio introduce LNGL, il primo calcolo per sequenti annidati lineari senza taglio per la logica di Gödel-Löb. Questo sistema opera su linee di sequenti di Gentzen e mantiene proprietà fondamentali come l'invertibilità e l'ammissibilità del taglio.
• Nuova Tecnica di Linearizzazione: L'autore presenta un metodo generale per estrarre sistemi di sequenti annidati lineari da sistemi di tree-ipersequenti. Si congettura che questa tecnica sia applicabile ad altri logiche modali e correlate per generare nuovi sistemi annidati lineari.
• Corrispondenza Proof-Teoretica Completa: Il saggio stabilisce una completa corrispondenza sintattica a sei vie tra i seguenti sistemi: $G3KGL$, $CSGL^*$, $LNGL$, $GL_{seq}$, $GL_\infty$ e $GL_{circ}$.
• Mappature Costruttive: Il lavoro fornisce la prima mappatura costruttiva delle prove tra sistemi strutturali (etichettati, tree-ipersequenti, annidati lineari) e il sistema di sequenti ciclici ($GL_{circ}$).

Risultati
Il risultato primario è la dimostrazione che le prove in uno qualsiasi dei sei principali sistemi di sequenti per GL possono essere trasformate sintatticamente in prove in qualsiasi altro. Nello specifico:

• Le prove in $CSGL^*$ possono essere trasformate in prove end-active, poi linearizzate in LNGL.
• Le prove in LNGL possono essere normalizzate e trasformate in $GL_{seq}$.
• Le prove in $GL_{seq}$ possono essere trasformate in $G3KGL$ e nei sistemi ciclici ($GL_{circ}$, $GL_\infty$).
• Il saggio conferma che $LNGL$ è corretto e completo per GL, e che le prove in $LNGL$ possono essere messe in una forma normale dove l'applicazione di regole modali e locali si ripete in stadi.

Significatività
Il saggio sostiene di "completare il quadro" delle corrispondenze proof-teoretiche per la logica di Gödel-Löb. Stabilendo queste trasformazioni sintattiche, il lavoro permette il trasferimento di risultati (come le proprietà di interpolazione o i limiti di complessità) tra i sistemi senza richiedere dimostrazioni indipendenti in ogni formalismo. Inoltre, l'introduzione di LNGL fornisce un nuovo strumento per la ricerca della prova con proprietà di complessità ottimali, mentre la tecnica di linearizzazione offre un potenziale percorso per generare sistemi annidati lineari per altre logiche. Il lavoro fornisce inoltre la prima mappatura costruttiva tra sistemi strutturali e prove cicliche, colmando un divario tra diversi approcci alla gestione del ragionamento induttivo/coinduttivo nella logica modale.