Wider systems for linear logic with fixed points: proof theory and complexity

1. Il Problema e il Contesto

Il lavoro si colloca nell'ambito della teoria della dimostrazione strutturale applicata alla Logica Lineare (MALL) estesa con operatori di punto fisso ($\mu$ per i punti fissi minimi e $\nu$ per i massimi).
Negli ultimi decenni, sono stati proposti diversi sistemi per gestire i punti fissi, inclusi sistemi con regole di induzione/co-induzione esplicite, prove cicliche (non ben fondate) e sistemi con regole a ramificazione infinita.
Il problema centrale affrontato dagli autori è l'estensione di questi sistemi a ramificazioni ordinate da un ordinale arbitrario $\alpha$ (computabile). Mentre lavori precedenti (es. [13, 11]) si limitavano alla ramificazione $\omega$-ordinata (adatta solo a modelli continui dove i punti fissi sono raggiunti in $\le \omega$ passi), questo studio considera modelli generali (come il calcolo modale $\mu$ o l'aritmetica) che ammettono ordinali di chiusura arbitrari.
La domanda fondamentale è: qual è la complessità algoritmica del problema della dimostrabilità (provability) nel sistema $\mu\text{MALL}_{\alpha,\alpha}$?

2. Metodologia

Gli autori adottano un approccio che combina fondamenti di teoria della dimostrazione con tecniche di teoria della complessità iperaritmetica.

• Definizione del Sistema ($\mu\text{MALL}_{\alpha,\alpha}$): Estendono la sintassi della logica lineare con punti fissi permettendo annotazioni ordinali sui connettivi $\mu$ e $\nu$ (es. $\mu_\beta x A$). Le regole di inferenza per $\nu_\beta$ hanno premesse indiziate da tutti gli $\gamma < \beta$, permettendo una ramificazione transfinita.
• Strumenti di Teoria della Dimostrazione:
  • Eliminazione del Taglio (Cut-Elimination): Dimostrano che ogni dimostrazione può essere trasformata in una senza regole di taglio.
  • Focussing (Focusing): Introducono una disciplina di focussing che organizza la ricerca delle dimostrazioni in fasi sincrone (non invertibili) e asincrone (invertibili), riducendo drasticamente lo spazio di ricerca.
  • Rango delle Formule (Formula Rank): Sviluppano una nuova nozione di "rango" basata sulle operazioni naturali sugli ordinali (somma naturale $\oplus$ e prodotto naturale $\otimes$). A differenza di approcci precedenti che usavano il massimo o la dimensione della formula, questo rango è calibrato per fornire un limite superiore stretto (tight bound) sull'altezza dello spazio di ricerca delle dimostrazioni senza taglio.
• Riduzioni Computazionali:
  • Per il limite superiore, codificano la ricerca di dimostrazioni come definizioni induttive positive e le collegano alla gerarchia iperaritmetica.
  • Per il limite inferiore, codificano le formule infinitarie computabili (che sono complete per i livelli della gerarchia iperaritmetica) all'interno del sistema logico, simulando macchine di Minsky e la verità di formule infinitarie.

3. Contributi Chiave

1. Fondamenti Teorici per Ramificazioni Ordinali:

   • Dimostrazione dell'eliminazione del taglio per $\mu\text{MALL}_{\alpha,\alpha}$ per ogni ordinale $\alpha$.
   • Dimostrazione del teorema di focussing, che garantisce che ogni dimostrazione ammette una forma normale focalizzata.
   • Definizione di un rango di formula preciso che garantisce che la ricerca di dimostrazioni senza taglio termini e fornisca stime quantitative sull'altezza delle prove.

2. Classificazione della Complessità:

   • Il risultato principale è la classificazione della complessità del problema della dimostrabilità per ordinali computabili $\alpha \ge \omega$.
   • Il sistema è completo per il livello $\Sigma^0_{\omega^\alpha \omega}$ della gerarchia iperaritmetica (sotto riduzioni di Turing).
   • Questo generalizza risultati precedenti: per $\alpha = \omega$, la complessità è $\Sigma^0_{\omega^\omega}$, mentre per $\alpha$ più grandi, la complessità cresce esponenzialmente in termini di iterazioni del salto di Turing.

3. Tecniche di Codifica:

   • Sviluppo di una codifica di macchine di Minsky all'interno della logica per simulare funzioni computabili parziali.
   • Costruzione di una formula induttiva (Ind) che simula la definizione di verità per le frasi infinitarie computabili, permettendo di ridurre il problema della verità di tali frasi alla dimostrabilità in $\mu\text{MALL}_{\alpha,\alpha}$.

4. Risultati Principali

• Teorema 2.8 (Completezza): Per ogni ordinale computabile $\alpha \ge \omega$, il problema della dimostrabilità in $\mu\text{MALL}_{\alpha,\alpha}$ è $\Sigma^0_{\omega^\alpha \omega}$-completo.
  • Limite Superiore: La dimostrabilità è in $\Sigma^0_{\omega^\alpha \omega}$ perché lo spazio delle dimostrazioni senza taglio può essere descritto da una definizione induttiva di rango $\omega^\alpha \omega$.
  • Limite Inferiore: Il problema è $\Sigma^0_{\omega^\alpha \omega}$-difficile (hard) perché si può ridurre il problema della verità delle frasi infinitarie computabili (complete per quel livello) alla dimostrabilità nel sistema, sfruttando la capacità del sistema di simulare la gerarchia di Kleene's O attraverso le ramificazioni ordinate.
• Corollario 8.1: Se $\omega \le \alpha < \omega^\omega$, allora la dimostrabilità è $\Sigma^0_{\omega^{\omega^\omega}}$-completa. Questo implica che per un'ampia classe di ordinali, il problema di decisione è Turing-equivalente.

5. Significato e Implicazioni

• Unificazione dei Modelli: Il lavoro fornisce un quadro unificato per confrontare diverse metodologie di ragionamento sui punti fissi (induzione esplicita, prove cicliche, ramificazione infinita) mostrando come la complessità dipenda direttamente dall'ordinale di chiusura consentito dal sistema.
• Precisione nella Complessità: Dimostra che la complessità della logica lineare con punti fissi non è fissa, ma scala con la potenza degli ordinali ammissibili. Questo offre una "scaletta" precisa di complessità iperaritmetica basata su proprietà logiche.
• Strumenti per la Teoria della Dimostrazione: L'introduzione di un rango basato sulle operazioni naturali sugli ordinali rappresenta un avanzamento tecnico significativo per il controllo della complessità delle dimostrazioni in sistemi infinitari, offrendo strumenti più raffinati rispetto alle semplici misure di dimensione.
• Confronto con Altre Logiche: Il paper nota che la logica di azione infinitaria con multiplexing (studiata in lavori correlati) ha una complessità significativamente inferiore ($\Sigma^0_{\omega^\omega}$), suggerendo che la combinazione specifica di connettivi lineari (moltiplicativi e additivi) con punti fissi transfiniti è ciò che genera l'alta complessità osservata.

In sintesi, questo articolo stabilisce un ponte rigoroso tra la struttura proof-theoretica di sistemi logici infinitari con punti fissi e la teoria della complessità computazionale, fornendo una mappa precisa della difficoltà algoritmica di tali sistemi in funzione dei loro parametri ordinali.