Uniform Interpolation of Basic Tense Logic

Sintesi Tecnica: Interpolazione Uniforme della Logica del Tempo Basica

Problema
Il saggio affronta il problema aperto di stabilire la proprietà di interpolazione uniforme per la logica del tempo basica (nota anche come logica modale bidirezionale o logica modale con conversa), indicata con $K_t$. Sebbene la proprietà di interpolazione di Craig per $K_t$ sia ben stabilita attraverso metodi sia proof-teoretici che semantici, la proprietà di interpolazione uniforme — che richiede l'esistenza di un "interpolante uniforme" $\exists p.\phi$ per ogni formula $\phi$ e variabile $p$ tale che $\exists p.\phi$ sia indipendente da $p$ e preservi le relazioni di provabilità con tutte le formule prive di $p$ — non era stata pienamente dimostrata per questa logica. L'autore osserva che, mentre Visser (1996) ha fornito un argomento semantico per l'interpolazione uniforme della logica modale basica $K$ utilizzando bisimulazioni stratificate, questo risultato non era stato esteso alla espansione temporale che coinvolge la modalità conversa.

Metodologia
Il saggio impiega un approccio semantico, estendendo l'argomento modello-teoretico di Visser basato su bisimulazioni stratificate (o limitate) al contesto della logica del tempo. La metodologia procede attraverso i seguenti passaggi:

1. Definizioni e Framework: L'autore definisce la sintassi e la semantica della logica del tempo basica, introducendo il sistema di Hilbert standard $H(K_t)$ e la semantica di Kripke con modalità in avanti ($\square$) e all'indietro ($\blacksquare$). Il concetto di bisimulazione stratificata è adattato per la logica del tempo, incorporando condizioni per le transizioni in avanti ($Forth$, $Back$) e all'indietro ($Forth^{-1}$, $Back^{-1}$), indicizzate per profondità modale $n$.
2. Proprietà di Espansione della Bisimulazione: Viene formulata una condizione sufficiente affinché una logica temporale normale $\Lambda_{\mathcal{F}}$ (associata a una classe di frame $\mathcal{F}$) possieda la proprietà di interpolazione uniforme. Tale condizione, denominata proprietà di espansione della bisimulazione, richiede che per ogni coppia di modelli puntati $(M_1, w_1)$ e $(M_2, w_2)$ in $\mathcal{F}$ che sono bisimili fino alla profondità $n$ su un insieme condiviso di variabili, esista un modello intermedio $(N, x)$ in $\mathcal{F}$ che li connetta tramite bisimulazioni sui rispettivi insiemi di variabili.
3. Costruzione del Modello Intermedio: Il nucleo del contributo tecnico consiste nel dimostrare che la classe di tutti i frame ($\mathcal{F}_{all}$) possiede la proprietà di espansione della bisimulazione. L'autore costruisce un modello intermedio $N$ prendendo l'unione disgiunta dei due modelli di input e aggiungendo un nuovo stato "universale" $T$ connesso a tutti gli stati. La relazione in $N$ è definita su uno spazio prodotto che coinvolge gli stati dei modelli originali e un indice di "strato", simulando efficacemente i passi di bisimulazione richiesti per soddisfare la proprietà di espansione.
4. Risultati di Trasferimento: Il saggio investiga la preservazione della proprietà di interpolazione uniforme sotto varie estensioni:
   • Immagini Speculari: Se una logica $\Lambda$ è invariante rispetto all'operazione di immagine speculare (scambio di $\square$ e $\blacksquare$), la proprietà si trasferisce alle estensioni per assiomi di immagine speculare.
   • Assiomi Costanti: La proprietà è preservata quando si aggiungono formule costanti (formule senza variabili proposizionali).
   • Traduzione Boxdot: La proprietà è mostrata essere trasferibile alla controparte riflessiva di una logica tramite la traduzione boxdot.
5. Costruzione del Contro-Esempio: Per dimostrare i limiti della proprietà, il saggio analizza l'espansione temporale della logica modale $S4$ (denotata $S4_t$). Utilizzando una specifica costruzione di modello (un cammino infinito con valori di verità alternati per una proposizione $r$) e un argomento di bisimulazione stratificata, l'autore dimostra che $S4_t$ manca della proprietà di interpolazione uniforme.

Contributi Chiave e Risultati

• Teorema Principale: Il saggio stabilisce che la logica del tempo basica minima $K_t$ possiede la proprietà di interpolazione uniforme. Ciò viene ottenuto dimostrando che la classe di tutti i frame soddisfa la proprietà di espansione della bisimulazione.
• Caratterizzazione Semantica: Viene dimostrato che l'interpolante uniforme in $K_t$ coincide con un quantificatore di bisimulazione. Nello specifico, una formula $\exists p.\phi$ è vera in uno stato se e solo se esiste un modello bisimile (dove $p$ è interpretato diversamente) in cui $\phi$ è vera.
• Estensione ai Sub-logiche: La proprietà di interpolazione uniforme è mostrata essere valida per varie estensioni di $K_t$, incluse quelle definite da assiomi costanti (ad esempio, esistenza di momenti iniziali/finali) ed estensioni invarianti per immagine speculare.
• Fallimento in $S4_t$: Il saggio dimostra che l'espansione temporale di $S4$ ($S4_t$) non possiede la proprietà di interpolazione uniforme. Questo risultato estende le precedenti scoperte di Ghilardi e Zawadowski su $S4$ al contesto temporale, mostrando che l'aggiunta degli assiomi di riflessività e transitività rompe la proprietà di interpolazione uniforme.
• Meccanismi di Trasferimento: Il saggio fornisce prove formali per il trasferimento della proprietà di interpolazione uniforme tramite immagini speculari, estensioni costanti e la traduzione boxdot, permettendo la derivazione di risultati per logiche come $K_t \oplus T_\square$ e $K_t \oplus 4_\square$ (sotto specifiche condizioni).

Significatività
Il saggio sostiene di risolvere una lacuna significativa nella letteratura riguardante le proprietà meta-logiche della logica del tempo basica. Estendendo l'argomento semantico di Visser al setting modale bidirezionale, l'autore conferma che $K_t$ gode della proprietà di interpolazione uniforme, un risultato precedentemente ignoto nonostante l'uso diffuso di questa logica in filosofia, informatica e semantica formale. Il lavoro chiarisce il confine tra le logiche che possiedono questa forte proprietà di interpolazione (come $K_t$) e quelle che non la possiedono (come $S4_t$), fornendo un robusto framework semantico (bisimulazioni stratificate) per analizzare l'interpolazione nelle logiche del tempo. Inoltre, il saggio suggerisce che l'interpolante uniforme in $K_t$ può essere compreso semanticamente come una versione temporale di un quantificatore di bisimulazione, offrendo una comprensione concettuale più profonda del potere espressivo della logica. I risultati pongono inoltre le basi per future investigazioni sull'interpolazione di Lyndon uniforme e sull'applicazione di queste tecniche a logiche del tempo multimodali e ibride.