Possibly Relevant Translations

Sintesi Tecnica: Possibili Traduzioni Rilevanti

Problema e Motivazione
Il saggio affronta la relazione strutturale tra le logiche rilevanti (specificamente la linea Anderson–Belnap) e le logiche modali normali. Mentre la traduzione della logica intuizionistica nella logica modale classica (tramite la traduzione di Gödel–McKinsey–Tarski) ha storicamente favorito un significativo scambio tra le tradizioni, una traduzione sistematica comparabile tra logiche rilevanti e modali rimane poco sviluppata. L'autore mira a stabilire traduzioni piene e fedeli dalle logiche rilevanti alle logiche modali normali per chiarire le connessioni strutturali, derivare risultati corollari e identificare i limiti degli attuali approcci traslazionali. Il lavoro si concentra inizialmente sul frammento positivo $\{\land, \lor, \to\}$ e si estende gradualmente per includere la costante di verità $t$, la fusione $\circ$ e la negazione $\neg$.

Metodologia
Il saggio impiega un approccio semantico, utilizzando trasformazioni di modelli tra due framework distinti:

1. Frame di Routley–Meyer: La semantica standard per le logiche rilevanti, definita come triple $(K, R, N)$ dove $R$ è una relazione ternaria e $N$ è un insieme di punti normali, soggetti a specifiche restrizioni relazionali e d'ordine (ad esempio, la condizione "down-down-up").
2. Frame di Kripke: La semantica standard per le logiche modali normali, definita come coppie $(W, R)$ (o tuple con relazioni aggiuntive per linguaggi estesi).

La metodologia centrale consiste nel definire una funzione di traduzione (denotata $\star$, $\ast$ o $\circ$) dalle formule rilevanti alle formule modali. Per dimostrare che queste traduzioni siano piene (se un'implicazione rilevante vale, la traduzione modale vale) e fedeli (se la tradità modale vale, l'implicazione rilevante vale), l'autore costruisce due trasformazioni di modelli:

• $F$: Mappa modelli di Kripke puntati in modelli di Routley–Meyer puntati.
• $G$: Mappa modelli di Routley–Meyer puntati in modelli di Kripke puntati.

Queste trasformazioni sono progettate per soddisfare schemi di adgiunzione in cui la soddisfazione in un modello corrisponde alla soddisfazione della formula tradotta nell'altro. Il saggio utilizza inoltre la teoria della corrispondenza (specificamente la corrispondenza di Sahlqvist) per identificare le condizioni di frame nella semantica di Kripke che corrispondono a specifici assiomi rilevanti.

Contributi Chiave e Risultati

1. Traduzione Positiva di Base ($\star$):

   • L'autore definisce una traduzione $\star$ per il frammento $\{\land, \lor, \to\}$ dove $\to$ è mappato in un operatore modale definito $\neg \Diamond(\cdot, \neg \cdot)$.
   • Teorema 1.4: Stabilisce che per la logica rilevante di base $B^+$ e la logica modale binaria di base $K_2$, $\vdash_{B^+} \phi \to \psi$ se e solo se $\vdash_{K_2} \phi^\star \supset \psi^\star$.
   • Estensione a Logiche Più Forti: La traduzione si estende a logiche assiomatizzate da sottoinsiemi di assiomi 7–10 (ad esempio, $TW^+$, $TWJ^+$, $C^+$). Tuttavia, il saggio dimostra che questa traduzione fallisce per le logiche che richiedono contrazione (assioma 11) o asserzione (assioma 12), come $R^+$. Il fallimento deriva dal fatto che la semantica di Kripke più semplice manca delle specifiche condizioni d'ordine (come la proprietà "down-down-up") inerenti ai frame di Routley–Meyer che sono necessarie per validare questi assiomi.

2. Traduzione di Implicazione Annidata ($\ast$):

   • Per affrontare le formule in cui il connettivo principale non è $\to$, viene introdotta una seconda traduzione $\ast$, che mappa $\phi \to \psi$ in $\Box_\to(\phi^\star \supset \psi^\star)$.
   • Teorema 1.7: Mostra che $\ast$ fornisce un embedding pieno e fedele di $B^+$ in $K_2$ per tutte le formule positive, realizzando $B^+$ come un frammento sintattico di $K_2$.
   • Come la traduzione $\star$, anche questo approccio incontra limitazioni quando esteso a logiche che coinvolgono contrazione e asserzione.

3. Indecidibilità e Interpolazione:

   • Il saggio trasferisce i risultati di indecidibilità dalle logiche rilevanti alle logiche modali. Nello specifico, dimostra che le logiche modali corrispondenti alle condizioni di frame di $TWJ^+$ e $C^+$ sono indecidibili (Teorema 1.9), integrando i risultati esistenti di Urquhart e altri.
   • L'autore solleva questioni aperte riguardanti la Proprietà di Interpolazione di Craig (CIP). Sebbene $K_2$ possieda la CIP, non è noto se $B^+$ la possieda. La traduzione suggerisce che, se $B^+$ manca della CIP, ciò potrebbe essere dovuto al comportamento specifico della traduzione o alla mancanza di un certo vocabolario.

4. Traduzioni Estese ($\circ$):

   • Per superare le limitazioni delle traduzioni precedenti riguardo a contrazione e asserzione, il saggio introduce una traduzione in un linguaggio modale più ricco contenente una modalità nulla $t$ e una modalità binaria $\circ$.
   • Definizione 2.2: Definisce la Logica Modale $B^+$ ($Mod.B^+$) come la minima logica modale normale contenente gli assiomi di residuazione e gli assiomi corrispondenti alle condizioni di frame di Routley–Meyer (riflessività, transitività, upset, ecc.).
   • Teorema 2.5: Dimostra che per il linguaggio esteso con $t$ e $\circ$, la traduzione $\circ$ è piena e fedele: $\vdash_B \phi$ se e solo se $\vdash_{Mod.B^+} t \supset \phi^\circ$. Questa traduzione cattura con successo i vincoli strutturali dei frame di Routley–Meyer (inclusa la relazione d'ordine $\leq$) all'interno della semantica di Kripke.
   • Teorema 2.8: Estende questo risultato al linguaggio completo includendo la negazione $\neg$ introducendo una modalità unaria $\Box_\neg$ e le corrispondenti condizioni di frame (involuzione e inversione dell'ordine).

Significatività e Rivendicazioni
Il saggio rivendica modestamente di chiarire le connessioni strutturali tra logiche rilevanti e modali attraverso una serie di traduzioni. La sua principale significatività risiede nel:

• Fornire una traduzione piena e fedele della logica rilevante di base $B$ (e delle sue estensioni con $t, \circ, \neg$) in una specifica logica modale normale ($Mod.B$), realizzando la logica rilevante come un frammento sintattico della logica modale.
• Evidenziare le limitazioni delle traduzioni più semplici (come $\star$) quando applicate a logiche rilevanti più forti (come $R^+$), notando specificamente che i frame di Kripke standard non possono catturare le necessarie proprietà d'ordine dei frame di Routley–Meyer senza assiomi o modalità aggiuntive.
• Facilitare il trasferimento di proprietà meta-logiche, come decidibilità e indecidibilità, tra le due tradizioni.
• Identificare questioni aperte per il lavoro futuro, in particolare riguardo alla proprietà di interpolazione in $B^+$ e al potenziale di approfondire la connessione strutturale includendo logiche incomplete rispetto al frame.

L'autore dichiara esplicitamente che il saggio è "esplorativo e ampio piuttosto che profondo", lasciando un'analisi più completa delle motivazioni filosofiche e delle relazioni strutturali più profonde a lavori futuri.