Glivenko's theorems from an ecumenical perspective

Sintesi Tecnica: I Teoremi di Glivenko da una Prospettica Ecumenica

Enunciato del Problema
Il lavoro affronta la relazione fondazionale tra logica classica (CL) e logica intuizionistica (IL), rivedendo specificamente i teoremi di Glivenko. Questi teoremi stabiliscono che se una formula è dimostrabile classicamente, la sua doppia negazione è dimostrabile intuizionisticamente, e se una formula negata è dimostrabile classicamente, essa è dimostrabile anche intuizionisticamente. Sebbene questi risultati siano ben compresi nel contesto di sistemi logici separati, il lavoro indaga come queste relazioni si manifestino all'interno di sistemi ecumenici. I sistemi ecumenici sono quadri unificati in cui logica classica e logica intuizionistica coesistono pacificamente senza collassare l'una nell'altra, spesso distinguendo operatori (ad esempio, disgiunzione classica vs. intuizionistica) o etichettando le formule per indicare la loro natura logica. Il problema centrale è determinare come i risultati di tipo Glivenko si traducano quando il ragionamento classico e quello intuizionistico sono integrati in un singolo sistema deduttivo, e analizzare le differenze tra due approcci principali all'ecumenismo: l'approccio "inferenzialista" (che distingue gli operatori) e l'approccio "generalista" (che distingue le formule tramite etichette).

Metodologia
Gli autori impiegano un'analisi dimostrativa-teorica utilizzando sistemi di Deduzione Naturale. Esaminano tre specifici quadri ecumenici:

1. NE (Sistema di Prawitz): Un approccio inferenzialista in cui logici classici e intuizionisti condividono operatori neutrali (congiunzione, quantificatore universale, negazione, assurdo) ma possiedono versioni distinte di operatori non neutrali (implicazione, disgiunzione, quantificatore esistenziale).
2. ECI (Sistema di Barroso-Nascimento): Un approccio generalista in cui viene utilizzato un unico insieme di operatori, ma le formule sono etichettate con una costante $c$ (ad esempio, $A^c$) per denotare il comportamento classico. Questo sistema è costruito sulla deduzione naturale intuizionistica integrata con regole di introduzione ($I_C$) ed eliminazione ($E_C$) per l'etichetta.
3. NEK (Sistema ispirato a Krauss): Una variazione del sistema di Prawitz che include una congiunzione classica ($\land_c$) e un quantificatore universale classico ($\forall_c$), basata su lavoro inedito di Krauss.

La metodologia prevede:

• Definire teoremi di tipo Glivenko interni a questi sistemi (relazionando operatori/formule classici ai loro corrispettivi intuizionistici).
• Costruire derivazioni per dimostrare queste relazioni interne.
• Definire funzioni di traduzione ($t_{ECI}$ e $t_{NEK}$) per mappare le formule tra i sistemi.
• Investigare l'equivalenza deduttiva di questi sistemi, in particolare nel frammento proposizionale rispetto al frammento del primo ordine che coinvolge la quantificazione universale.

Contributi e Risultati Chiave

1. Teoremi di Glivenko Interni in NE:
   Gli autori dimostrano che nel sistema di Prawitz (NE), dove esistono operatori distinti, vale internamente una relazione di "tipo Glivenko". Per qualsiasi formula $C$ il cui operatore principale è classico, $C \vdash_{NE} \neg\neg C^*$, dove $C^*$ è la formula con l'operatore classico sostituito dal suo corrispettivo intuizionistico. Questo vale per la disgiunzione classica ($\lor_c$), l'implicazione ($\to_c$) e la quantificazione esistenziale ($\exists_c$). Un risultato corrispondente vale per le formule negated: $\neg C \vdash_{NE} \neg C^*$.

2. Trivialità dei Risultati di Glivenko in ECI:
   Nel sistema ECI, la relazione tra una formula classica $A^c$ e il suo corrispettivo intuizionistico è strutturalmente banale. Le regole del sistema producono immediatamente $A^c \vdash_{ECI} \neg\neg A$. Di conseguenza, la traduzione $t_{ECI}$, che mappa $A^c$ in $\neg\neg A$, riduce il problema della normalizzazione in ECI a quello della logica intuizionistica. Gli autori mostrano che, sebbene questa traduzione funzioni per la logica proposizionale, essa oscura la posizione specifica del ragionamento classico in una derivazione, a meno che la derivazione non venga attentamente ricostruita per tracciare la "natura classica" delle formule derivate.

3. Il Caso della Congiunzione Classica e NEK:
   Il lavoro introduce NEK, che aggiunge la congiunzione classica ($\land_c$) al sistema di Prawitz. Gli autori dimostrano che $\land_c$ soddisfa i teoremi di Glivenko interni ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). Mostrano inoltre che nel frammento proposizionale (o nella logica del primo ordine senza quantificatori universali), NEK e ECI sono deduttivamente equivalenti. Questa equivalenza è stabilita tramite una traduzione $t_{NEK}$ che mappa gli operatori classici in NEK su formule etichettate in ECI.

4. La Divergenza con la Quantificazione Universale:
   Un risultato critico è il fallimento dell'equivalenza deduttiva tra NEK e ECI quando viene introdotta la quantificazione universale.

   • In NEK, il quantificatore universale classico $\forall_c$ è definito tramite regole armoniche con la logica intuizionistica. Tuttavia, il teorema di Glivenko interno fallisce per $\forall_c$: $\vdash_{NEK} \forall_c x A(x)$ non implica $\vdash_{NEK} \neg\neg \forall_i x A(x)$.
   • In ECI, la formula etichettata $(\forall x A(x))^c$ si comporta diversamente. A causa delle regole del sistema, vale $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$.
   • Gli autori spiegano questa discrepanza: in NEK, $\forall_c x A(x)$ è interpretato come $\neg \exists x \neg A(x)$, mentre in ECI, $(\forall x A(x))^c$ è effettivamente interpretato come $\neg\neg \forall x A(x)$. Questi non sono equivalenti intuizionisticamente. Il lavoro sostiene che la "trivialità" dei risultati di Glivenko in ECI per le formule universali nasce dal fatto che l'etichetta $c$ forza un'interpretazione a doppia negazione che non si allinea con il comportamento semantico del quantificatore universale classico nell'approccio inferenzialista.

Significato e Affermazioni
Il lavoro afferma che la prospettiva ecumenica offre una comprensione più profonda dell'interazione tra ragionamento classico e intuizionistico. Confrontando gli approcci "inferenzialista" (NE/NEK) e "generalista" (ECI), gli autori evidenziano una differenza concettuale sottile ma significativa:

• I sistemi inferenzialisti (Prawitz/Krauss) cambiano direttamente il significato dei connettivi fornendo regole di introduzione ed eliminazione distinte per gli operatori classici.
• I sistemi generalisti (ECI) cambiano il livello della prova, dotando la logica intuizionistica di mezzi classici di prova (tramite l'etichetta $c$) che alterano indirettamente il significato degli operatori.

Gli autori concludono che, sebbene questi approcci siano equivalenti nella logica proposizionale, divergono in presenza di quantificazione universale. Questa divergenza suggerisce che la scelta del quadro ecumenico non è meramente una preferenza notazionale, ma influisce sul comportamento logico dei quantificatori. Il lavoro postula che la prospettiva ecumenica aiuta a identificare esattamente dove il ragionamento classico è necessario e chiarisce che i principi classici e intuizionistici possono coesistere senza che l'uno collassi nell'altro, a condizione che il sistema sia costruito con attenzione a questi principi inferenziali distinti.