A non-uniform view of Craig interpolation in modal logics with linear frames

Sintesi Tecnica: Una visione non uniforme dell'interpolazione di Craig nelle logiche modali con frame lineari

Enunciato del Problema
La Proprietà di Interpolazione di Craig (CIP) è una proprietà fondamentale nella logica che afferma che, per ogni implicazione valida $\phi \to \psi$, esiste un interpolante $\iota$ che utilizza solo il vocabolario condiviso di $\phi$ e $\psi$ tale che $\phi \to \iota$ e $\iota \to \psi$ siano anch'essi validi. È un fatto "negativo" ben consolidato che molte logiche modali normali che estendono K4.3 (la logica dei frame lineari transitivi) mancano della CIP, in particolare quelle con profondità illimitata. Tradizionalmente, l'assenza della CIP ha posto fine alla ricerca di interpolanti per una data logica.

Questo articolo inquadra l'assenza della CIP come una questione di ricerca investigando il Problema dell'Esistenza dell'Interpolante (IEP): dato due formule $\phi$ e $\psi$ tali che $\phi \to \psi$ sia valida in una logica $L$, esiste un interpolante di Craig in $L$? A differenza della CIP uniforme, l'IEP non si riduce al semplice controllo di validità perché la validità dell'implicazione non garantisce l'esistenza di un interpolante. La domanda centrale affrontata è se l'IEP sia computazionalmente più difficile del problema di validità (entailment) per queste logiche. Risultati precedenti su altre logiche (ad es., logiche modali con nominali, frammenti della logica del primo ordine) hanno suggerito che l'IEP potrebbe essere significativamente più difficile (ad es., 3ExpTime). Questo articolo indaga se ciò sia vero per le logiche modali proposizionali contenenti K4.3.

Metodologia
Gli autori impiegano un approccio non uniforme e modello-teoretico basato su bisimulazioni e frame descrittivi.

1. Caratterizzazione per Bisimulazione: Il saggio utilizza un criterio noto (Teorema 3.2) affermando che $\phi \to \psi$ manca di un interpolante in $L$ se e solo se esistono due modelli, $M_1$ e $M_2$, basati su frame descrittivi per $L$, tali che $M_1$ soddisfi $\phi$, $M_2$ soddisfi $\neg\psi$, e i punti radice di questi modelli siano $\sigma$-bisimili (dove $\sigma$ è la firma condivisa).
2. Frame Descrittivi: L'analisi si basa fortemente sulla struttura dei frame descrittivi (frame dotati di un'algebra specifica di insiemi interni che soddisfano condizioni di differenziazione, compattezza e densità/tightness). Ciò è crucialo perché, per logiche come GL.3 e Log{(N, <)}, i controesempi alla CIP non possono essere testimoniati da standard frame di Kripke ma richiedono frame descrittivi infiniti.
3. Decomposizione Strutturale: L'innovazione tecnica centrale consiste nell'analizzare la struttura di questi modelli bisimili. Gli autori partizionano i modelli in $\sigma$-blocchi (intervalli di punti con specifiche proprietà di bisimulazione) e dimostrano che qualsiasi coppia di modelli bisimili che testimonia la mancanza di un interpolante può essere trasformata in una coppia di modelli "quasi-finiti". Questi modelli sono costruiti come somme ordinate di modelli semplici basati su frame atomici (catene finite, cluster finiti o strutture "tadpole" come $C(\bigcirc_k, \bullet)$).
4. Proprietà Quasi-Polisize: Per le logiche finitamente assiomatizzabili, gli autori dimostrano che questi modelli testimoni possono essere limitati in dimensione da un polinomio della dimensione delle formule di input e degli assiomi della logica. Questo è denominato proprietà del modello bisimile quasi-polysize.

Contributi Chiave e Risultati

• Decidibilità e Complessità: Il saggio dimostra che per tutte le logiche modali normali finitamente assiomatizzabili contenenti K4.3, l'IEP è decidibile e coNP-completo.

  • Questo risultato è significativo perché mostra che l'IEP non è più difficile del problema di validità (che è anch'esso in coNP per queste logiche). Ciò contrasta nettamente con i recenti risultati di interpolazione non uniforme in altri framework logici dove l'IEP è strettamente più difficile.
  • La prova prevede un algoritmo non deterministico che ipotizza modelli di dimensione polinomiale che soddisfano il criterio di bisimulazione e verifica gli assiomi della logica.

• Proprietà del Modello Bisimile Quasi-Polysize: Gli autori stabiliscono che tutte le estensioni finitamente assiomatizzabili di K4.3 possiedono la "quasi-polysize bisimilar model property". Ciò significa che se un interpolante non esiste, esiste una coppia di modelli bisimili che testimonia questo fatto, dove i modelli sono somme ordinate di un numero polinomiale di modelli semplici basati su frame atomici di dimensione polinomiale.

  • Per le logiche di subframe co-persistenti d-persistenti (una sottoclasse), la proprietà è ancora più forte: esse possiedono la polysize bisimilar model property, dove i modelli sono standard frame di Kripke di dimensione polinomiale.

• Estensione alle Logiche Temporali Priane: La metodologia viene estesa alle logiche temporali priane (che contengono sia modalità di futuro che di passato) su flussi temporali standard:

  • Lin (tutti i frame lineari), LinQ (razionali) e LinR (reali): Queste logiche sono mostrate possedere la polysize bisimilar model property, e il loro IEP è coNP-completo.
  • Lin<ω (ordini lineari stretti finiti) e LinZ (numeri interi): Queste logiche non possiedono la proprietà polysize ma possiedono la quasi-polysize bisimilar model property. Anche il loro IEP è dimostrato essere coNP-completo.
  • La prova per le logiche temporali richiede la gestione di catene bidirezionali e cluster limite in entrambe le direzioni, necessitando di nuovi costrutti di frame (ad es., frame "tadpole" simmetrici $C(\bullet, \bigcirc_k, \bullet)$).

Significatività e Rivendicazioni
Il saggio sostiene di fornire il primo risultato generale sull'esistenza dell'interpolante di Craig che copre una vasta famiglia di logiche modali (estensioni di K4.3) che mancano della CIP. Dimostrando che l'IEP è coNP-completo per queste logiche, gli autori sfidano l'intuizione secondo cui l'assenza della CIP porti necessariamente a una classe di complessità superiore per il problema dell'esistenza.

Il lavoro suggerisce che la complessità dell'IEP non è intrinsecamente legata al fallimento della CIP, ma dipende dalle proprietà strutturali dei modelli necessari per testimoniare il fallimento. Gli autori pongono questo come un passo verso una classificazione delle logiche modali basata sulla complessità del loro IEP.

Il saggio nota esplicitamente che la sua prova non è costruttiva riguardo al calcolo degli interpolanti; fornisce una procedura di decisione per l'esistenza ma non offre un algoritmo efficiente per calcolare l'interpolante stesso o i limiti superiori sulla sua dimensione. Gli autori sottolineano inoltre che i frame descrittivi sono essenziali per le loro prove, sollevando la questione aperta se i frame di Kripke siano sufficienti per l'IEP in logiche che non sono d-persistenti ma sono fortemente Kripke-complete (come LinR).