Four intuitionistic modal connectives

Sintesi Tecnica: Quattro Connettivi Modali Intuizionistici

Enunciato del Problema
Il saggio affronta la semantica fondamentale e l'assiomatizzazione delle Logiche Modali Intuizionistiche (IML). Tradizionalmente, le IML interpretano i connettivi modali all'interno di strutture relazionali $(W, \leq, R, V)$, dove $\leq$ è un preordine e $R$ è una relazione binaria. Esiste una tensione centrale tra due grandi scuole di pensiero riguardanti l'operatore di possibilità:

1. L'approccio di Fischer Servi: definisce la possibilità ($\diamond_{FS}$) tale che $s \models \diamond_{FS} A$ se e solo se esiste un $t$ tale che $sRt$e$t \models A$. Questo approccio richiede tipicamente di limitare la classe di modelli ai frame "confluenti in avanti e all'indietro" per soddisfare la Proprietà di Ereditarietà (monotonicità rispetto a $\leq$).
2. L'approccio di Wijesekera: definisce la possibilità ($\diamond_{W}$) tale che $s \models \diamond_{W} A$ se e solo se per ogni $t \geq s$, esiste un $u$ tale che $tRu$e$u \models A$. Questo approccio non richiede strettamente la confluenza affinché la Proprietà di Ereditarietà sia soddisfatta.

Gli autori sostengono che limitare la discussione ai modelli confluenti (come fa Fischer Servi) sia una scelta arbitraria che privilegia una variante rispetto ad altre della Logica Primo Ordine Intuizionistica. Inoltre, osservano che la traduzione standard delle IML nella logica del primo ordine spesso fallisce nel catturare la semantica intesa se limitata solo ai modelli confluenti. Di conseguenza, il saggio cerca di stabilire un quadro unificato che incorpori quattro distinti connettivi modali senza limitare a priori la classe di frame, esplorando così l'intero panorama delle modalità intuizionistiche.

Metodologia
Gli autori impiegano una combinazione rigorosa di semantica relazionale, teoria della corrispondenza, sistemi di prova algebrica e tecniche modello-teoretiche:

1. Sintassi e Semantica:

   • Introducono un linguaggio contenente i connettivi intuizionistici standard ($\to, \top, \bot, \lor, \land$) e una doppia implicazione/co-implicazione ($\leftarrow$).
   • Sono definiti quattro operatori modali:
     • $\Diamond$ (possibilità in stile Přenosil): $s \models \Diamond A$ se e solo se $\exists t \leq s, \exists u (tRu \land u \models A)$.
     • $\Box$ (necessità in stile Fischer Servi): $s \models \Box A$ se e solo se $\forall t \geq s, \forall u (tRu \to u \models A)$.
     • $\Diamond$ (possibilità in stile Wijesekera): $s \models \Diamond A$ se e solo se $\forall t \geq s, \exists u (tRu \land u \models A)$.
     • $\blacksquare$ (doppia necessità): $s \models \blacksquare A$ se e solo se $\exists t \leq s, \forall u (tRu \to u \models A)$.
   • La semantica è definita sulla classe di tutti i frame (senza restrizioni di confluenza), e la Proprietà di Ereditarietà è dimostrata essere valida per tutte le formule sotto queste definizioni.

2. Teoria della Corrispondenza:

   • Il saggio investiga la definibilità modale di classi elementari di frame (es. seriali, riflessivi, simmetrici, transitivi, confluenti).
   • Utilizza formule firmate e regole di inferenza per caratterizzare le proprietà dei frame.
   • Impiega la "Proprietà di Relativizzazione" dalla teoria dei modelli per dimostrare l'indecidibilità del problema di definibilità modale per certe classi di frame.

3. Assiomatizzazione e Completezza:

   • Viene presentato un sistema di tipo Hilbert utilizzando insiemi di formule firmate (positive e negative), chiusi per sostituzione uniforme e specifiche regole di inferenza (incluse le regole per la doppia implicazione e l'interazione tra le modalità).
   • Gli autori costruiscono un Modello Canonico utilizzando "balanced clips" (triple composte da un filtro primo, un ideale primo e formule ausiliarie). Questa costruzione è necessaria per gestire le complesse interazioni tra le quattro modalità e la doppia implicazione.
   • I teoremi di completezza sono dimostrati per la logica minimale e le sue estensioni corrispondenti a specifiche classi di frame (riflessivi, seriali, confluenti in avanti/verso il basso).

4. Decidibilità:

   • Per provare la decidibilità, gli autori incorporano la IML minimale nel Frammento Guardato Monadico a Due Variabili della Logica Classica del Primo Ordine.
   • Definiscono funzioni di traduzione che mappano le formule intuizionistiche in formule del primo ordine guardate, sfruttando la nota decidibilità del frammento guardato.

Contributi Chiave e Risultati

• Quadro Unificato: Il saggio integra con successo quattro distinti connettivi modali ($\Diamond, \Box, \Diamond, \blacksquare$) in un unico quadro intuizionistico, dimostrando che essi non sono interdefinibili sulla classe di tutti i frame.
• Analisi dell'Eliminabilità: Si mostra che, sulla classe di frame confluenti in avanti e verso il basso ($C_{fd}$), tutti e quattro i connettivi sono eliminabili (interdefinibili). Tuttavia, su classi più ampie (come $C_{bdu}$), essi sono distinti.
• Risultati di Corrispondenza:
  • Le classi di frame confluenti in avanti ($C_f$) e verso il basso ($C_d$) sono positivamente definibili.
  • Le classi di frame riflessivi ($C_{ref}$), simmetrici ($C_{sym}$), transitivi ($C_{tra}$), euclidei ($C_{Euc}$) e deterministici ($C_{det}$) non sono modali definibili rispetto alla classe di tutti i frame (o specifiche sottoclassi come $C_{fbdu}$).
  • Le classi di frame confluenti all'indietro ($C_b$) e verso l'alto ($C_u$) non sono modali definibili rispetto a $C_{fd}$.
• Assiomatizzazione: Il saggio fornisce assiomatizzazioni complete per la logica minimale ($L_{min}$) e le sue estensioni corrispondenti a proprietà di riflessività, serialità e confluenza. La logica minimale è mostrata essere la logica di tutti i frame.
• Decidibilità: La decidibilità del problema dell'appartenenza per la logica modale intuizionistica minimale ($L_{min}$) e per diverse delle sue estensioni (riflessiva, seriale, confluenza) è provata essere decidibile. Ciò viene ottenuto riducendo il problema alla soddisfacibilità del Frammento Guardato Monadico a Due Variabili.
• Indecidibilità della Definibilità: Il saggio dimostra che i problemi decisionali per determinare se una classe elementare di frame è modale, positivamente o negativamente definibile sono indecidibili.

Significato e Rivendicazioni

Gli autori affermano che il loro lavoro fornisce una base più naturale e meno restrittiva per le IML evitando la limitazione arbitraria ai modelli confluenti. Introducendo la doppia implicazione e i quattro connettivi modali, essi offrono un linguaggio simmetrico e completo che cattura l'intero spettro dei comportamenti modali intuizionistici.

Il saggio nota con modestia che, sebbene la decidibilità della logica minimale sia stata stabilita, la classe di complessità di questo problema rimane una questione aperta. Inoltre, gli autori evidenziano che, sebbene certe regole di inferenza (specificamente $R8+$ e $R8-$) siano state utilizzate nelle prove di completezza, non è attualmente noto se queste regole possano essere sostituite da un insieme finito di assiomi. Pongono inoltre quesiti aperti riguardo alla finita assiomatizzabilità delle logiche corrispondenti ai frame simmetrici e transitivi, nonché il potenziale di adattare le tecniche di filtraggio a questo specifico contesto.

Questo lavoro serve come passo fondamentale per comprendere l'interazione tra le diverse semantiche modali intuizionistiche e le loro proprietà di frame, andando oltre la tradizionale dicotomia tra Fischer Servi e Wijesekera.