Riepilogo Tecnico: Dimostrazioni Non Ben Fondate Coalgebriche: Ricorsività e GTC

Enunciato del Problema

I sistemi di dimostrazione non ben fondati, incluse le dimostrazioni cicliche, sono essenziali per le logiche che coinvolgono la (co)induzione, come il calcolo modale $\mu$ e le logiche di punto fisso di ordine superiore. A differenza delle dimostrazioni finitarie con alberi di derivazione finiti, questi sistemi ammettono alberi di derivazione infiniti. Di conseguenza, la correttezza non può essere stabilita tramite la solita induzione strutturale sulla profondità dell'albero. Invece, questi sistemi impongono una Condizione di Traccia Globale (GTC), un vincolo sui percorsi infiniti all'interno degli alberi di derivazione, per garantire la correttezza.

Nonostante i vari approcci categoriali alle dimostrazioni cicliche (ad esempio, categorie $\mu$-bicomplete, categorie di traccia), fornire una caratterizzazione categoriale della GTC che garantisca la correttezza rimane una sfida significativa. Le principali difficoltà sono:

1. Globale vs Locale: La GTC impone vincoli su interi alberi di derivazione, il che è in conflitto con la natura locale e composizionale del ragionamento categoriale standard.
2. Struttura Infinitaria: Le dimostrazioni non ben fondate possono essere infinite, impedendo l'uso dell'induzione strutturale standard per costruire morfismi semantici.
3. Lacuna nella Teoria Coalgebrica Ricorsiva: Mentre le coalgebre ricorsive e ben fondate garantiscono soluzioni uniche (interpretazioni semantiche), gli alberi di derivazione delle dimostrazioni non ben fondate spesso producono coalgebre non ben fondate. Le teorie esistenti non spiegano in modo diretto perché esistano soluzioni uniche in casi specifici non ben fondati (ad esempio, l'esempio della "sequenza discendente" di Capretta e Jeannin et al.).

Metodologia

Il documento sviluppa un quadro coalgebrico per i sistemi di dimostrazione non ben fondati, modellando gli alberi di derivazione come coalgebre e formulando la GTC come condizione sui grafi di queste coalgebre.

1. Coalgebre di Functori Familiari su Presheaf

Gli autori modellano gli alberi di derivazione come coalgebre $c: C \to FC$ dove $F$ è un functore familiare su una categoria di presheaf $\widehat{\mathcal{J}}$.

• Functori Familiari: Sono generalizzazioni dei funtori polinomiali definiti tramite polinomi (diagrammi di categorie con proprietà di fibrazione specifiche). Consentono di etichettare i nodi con giudizi e di determinare le strutture di diramazione tramite regole di inferenza, adattando naturalmente parametri e contesti.
• Grafici di Coalgebre: Costruendo sulla nozione di grafi di coalgebre, il documento estende l'equivalenza tra la ben fondatezza delle coalgebre e l'assenza di percorsi infiniti nei loro grafi associati agli endofunctori sulle categorie di presheaf (Teorema 1.9).

2. Adjunzioni e Immagini Ricorsive

Per affrontare la natura non ben fondata delle dimostrazioni, il quadro sfrutta la corrispondenza dei morfismi da coalgebra ad algebra lungo le adjunzioni.

• Strategia: Invece di richiedere che la coalgebra originale $c$ sia ricorsiva, il documento investiga se la sua immagine sotto un adeguato adjunto sinistro $L$ (specificamente, un funtore di cambio di base indotto da un'annotazione ordinale) sia ricorsiva.
• Meccanismo: Se $Coalg(L)(c)$ è ricorsiva, e l'algebra semantica target $a$ giace nell'immagine dell'adjunto destro $R$ (cioè $a \cong Alg(R)(a')$), allora esiste un unico morfismo da coalgebra ad algebra per $c$ (Proposizione 2.4).
• Intuizione: Ciò corrisponde ad arricchire il grafo di derivazione con una dimensione aggiuntiva (annotazioni ordinali) ottenuta tirando indietro lungo un'adjunzione. Questa espansione può rendere il grafo ben fondato anche se l'originale non lo è.

3. Strutture di Traccia e GTC

La GTC è formalizzata utilizzando strutture di traccia $(pfml, prog)$:

• Struttura di Traccia: Un morfismo nella categoria dei polinomi ($VPoly$) che traccia le formule (o le formule marcate) lungo gli spigoli, combinato con un sottoinsieme di spigoli "progressivi" (tipicamente corrispondenti a sviluppi di punto fisso).
• Definizione di GTC: Una pre-dimostrazione soddisfa la GTC se ogni percorso infinito nel suo grafo etichettato ammette una traccia progressiva infinita lungo un suffisso.
• Annotazioni Ordinali: Il quadro costruisce un sistema di dimostrazione astratto $P^\gamma$ con giudizi annotati da ordinali. Il funtore dimenticante $u_\gamma: \mathcal{J}dg^\gamma \to \mathcal{J}dg$ induce l'adjunzione necessaria.

Contributi e Risultati Chiave

1. Estensione della Teoria dei Grafi ai Presheaf

Il documento estende l'equivalenza tra la ben fondatezza dei grafi e la ricorsività delle coalgebre dagli endofunctori su $\mathbf{Set}$ agli endofunctori sulle categorie di presheaf (Teorema 1.9). Ciò è ottenuto definendo i grafi delle coalgebre per funtori familiari e dimostrando che il funtore preserva le intersezioni e le immagini inverse.

2. Correttezza tramite Immagini Ricorsive

Il documento stabilisce un Teorema di Correttezza (Teorema 4.13): Se una pre-dimostrazione $c$ soddisfa la GTC, allora esiste un unico morfismo da coalgebra ad algebra da $c$ a qualsiasi algebra semantica $a$ (purché $a$ sia nell'immagine dell'algebra sollevata tramite annotazioni ordinali).

• Ciò fornisce una spiegazione coalgebrica per esempi non ben fondati (come la sequenza discendente) che ammettono soluzioni uniche ma non sono ricorsivi nel senso standard.
• Dimostra che la GTC garantisce che la coalgebra "espansa" (con annotazioni ordinali) diventi ricorsiva.

3. Caratterizzazione di GTC e Ricorsività

Il documento stabilisce una caratterizzazione bidirezionale tra la GTC e la ricorsività:

• GTC $\implies$ Ricorsività: Una pre-dimostrazione soddisfa la GTC se e solo se la sua immagine sotto il funtore di annotazione ordinale è ricorsiva (Teorema 4.17).
• Ricorsività $\implies$ GTC: Una pre-dimostrazione è ricorsiva se e solo se soddisfa la GTC per tutte le strutture di traccia (Proposizione 4.14).
• Ciò chiarisce che la GTC è essenzialmente la condizione che garantisce che, dopo il trasporto lungo un'adjunzione adeguata, la coalgebra rilevante diventi ricorsiva.

4. Istantanee Concrete

Il quadro è dimostrato attraverso tre sistemi di dimostrazione:

1. Calcolo modale $\mu$: Un sistema di dimostrazione non ben fondato in cui la GTC corrisponde all'esistenza di un $\nu$-thread (sviluppo infinito di un punto fisso massimo). Le annotazioni ordinali corrispondono agli approssimanti standard per i punti fissi massimi.
2. Logiche di Punto Fisso di Ordine Superiore (HFLN): Un sistema che richiede il tracciamento sia di tracce $\mu$ che $\nu$, dimostrando la capacità del quadro di gestire strutture di traccia complesse.
3. Categorie $\mu$-bicomplete: Una variante non ben fondata del sistema di dimostrazione circolare di Santocanale, che illustra la capacità del quadro di gestire categorie non discrete di giudizi (dove i giudizi variano funtorialmente con le assegnazioni di variabili).

Significato e Affermazioni

Il documento afferma che il suo contributo principale è un'astrazione categoriale delle dimostrazioni non ben fondate che garantisce con successo la correttezza.

• Insight Concettuale: La GTC non è semplicemente un controllo operativo, ma una proprietà strutturale che garantisce che la coalgebra diventi ricorsiva quando osservata attraverso la lente di un'adjunzione adeguata (specificamente, una guidata dalla semantica ordinale).
• Unificazione: Il quadro unifica il trattamento della correttezza per vari sistemi di dimostrazione non ben fondati sotto un unico meccanismo coalgebrico che coinvolge funtori familiari e adjunzioni.
• Colmatura di Lacune Teoriche: Colma la lacuna nelle teorie esistenti delle coalgebre ricorsive spiegando come soluzioni uniche possano esistere per coalgebre non ben fondate tramite il "sollevamento" della semantica lungo le adjunzioni.

Gli autori notano che, sebbene il quadro stabilisca la correttezza, è necessario un lavoro futuro per affrontare la completezza, l'eliminazione del taglio e altre condizioni di correttezza come le condizioni di reset o i thread rimbalzanti all'interno di questo contesto coalgebrico.