Classical Logic as Intuitionistic Logic with Duality

Sintesi Tecnica: La Logica Classica come Logica Intuizionista con Dualità

1. Il Problema
Il saggio affronta una sfida fondamentale nella teoria del significato: fornire una semantica proof-theoretic (P-tS) per la logica classica che aderisca a principi anti-realisti (costruttivisti) senza presupporre il principio di bivalenza o la verità trascendente la verificazione. Sebbene Sandqvist abbia sviluppato con successo una semantica di base-estensione (B-eS) per la logica intuizionista (IPL) e una versione per la logica classica (CPL), rimangono delle limitazioni. La semantica CPL di Sandqvist è limitata a connettivi specifici (inizialmente $\to, \bot, \forall$) e si basa su una dimostrazione di completezza tecnicamente complessa che coinvolge l'induzione su barra (bar induction). Inoltre, gli approcci esistenti spesso faticano a trattare il linguaggio proposizionale completo (inclusi $\lor$ ed $\exists$) in modo costruttivo. Gli autori mirano a risolvere questo problema offrendo una B-eS per la logica proposizionale classica completa che mantenga una dimostrazione di completezza elementare e costruttiva, rispondendo così alla sfida di Dummett riguardo al coordinamento tra inferenza classica e significato anti-realista.

2. Metodologia e Quadro Filosofico
Gli autori propongono un quadro bilateralista in cui la logica classica è concepita come "Logica Intuizionista + Dualità". Questo approccio si distacca dalle visioni tradizionali distinguendo tra contenuto e forza illocutoria a livello atomico, pur trattando le formule complesse come strutture logico-grammaticali piuttosto che come proposizioni dotate di forza in sé.

• Letterali come Proposizioni: Il sistema introduce i "letterali" ($L$) come gli unici oggetti di asserzione e negazione. Un contenuto $c$ è accoppiato a una forza per formare un letterale positivo ($c^+$, asserzione) o un letterale negativo ($c^-$, negazione). Fondamentalmente, la dualità è primitiva: $c^+$ e $c^-$ sono atti linguistici atomici indipendenti, non definiti tramite la negazione ($\neg$).
• Strutture Logico-Grammaticali: Le formule complesse (ad es. $\phi \land \psi$) non sono proposizioni da asserire o negare, ma strutture che organizzano il ragionamento. Di conseguenza, la distinzione bilaterale (asserzione vs. negazione) è ristretta al livello atomico (letterali).
• Dualità Inferenziale: La classicità viene recuperata non aggiungendo una semantica dei valori di verità, ma introducendo due principi inferenziali armoniosi a livello atomico (seguendo Negri e von Plato):
  1. Esclusione (EXC1): Asserire e negare lo stesso contenuto conduce all'assurdo ($l, l^\perp \vdash \bot$).
  2. Analisi dei Casi (EXC2): Se una conclusione segue sia da un'asserzione che dalla sua negazione duale, essa segue direttamente ($l \vdash \phi, l^\perp \vdash \phi \implies \vdash \phi$).

3. Sviluppo Tecnico

• Sistema di Deduzione Naturale ($NK^\pm$): Gli autori definiscono un sistema di deduzione naturale composto dalle regole intuizionistiche standard ($NJ$) più le regole di dualità atomica (EXC1 e EXC2). Questo sistema tratta i letterali come base, con formule complesse costruite tramite i connettivi standard.
• Semantica di Base-Estensione (B-eS):
  • Basi ($B$): Una base è un insieme di regole atomiche (relazioni inferenziali tra letterali).
  • Derivabilità ($\vdash_B$): La derivabilità in una base è definita induttivamente. Include le regole strutturali standard (riflessività, applicazione) e le due nuove clausole (exc1, exc2) che impongono la dualità a livello di letterale.
  • Supporto ($\Vdash_B$): La validità di una formula è definita induttivamente sulla struttura delle formule. Fondamentalmente, le clausole di supporto per i connettivi ($\to, \land, \lor$) sono identiche alle definizioni intuizioniste di Sandqvist. Il carattere classico della semantica è trasportato interamente dalle clausole di dualità nella definizione della derivabilità nella base, non dalle clausole di supporto per le formule complesse.
  • Validità ($\Gamma \Vdash \phi$): Una formula è valida se è supportata in ogni base.

4. Risultati Chiave

• Soundness (Teorema 5.1): Il sistema è sound (corretto): se $\Gamma \vdash_{NK^\pm} \phi$, allora $\Gamma \Vdash \phi$. La dimostrazione procede per induzione sulla derivazione, mostrando che le regole classiche (EXC1, EXC2) preservano il supporto.
• Completezza (Teorema za 6.2): Il sistema è completo: se $\Gamma \Vdash \phi$, allora $\Gamma \vdash_{NK^\pm} \phi$.
  • La dimostrazione adatta il metodo elementare di Sandqvist per la logica intuizionista.
  • Utilizza una "base di simulazione" ($\mathcal{N}$) costruita dai sottoprogrammi del sequente.
  • Un operatore di "appiattimento" (flattening) mappa le formule complesse in letterali atomici all'interno della base di simulazione.
  • Il lemma di "Naturalizzazione" dimostra che la derivabilità nella base di simulazione può essere tradotta nuovamente in derivabilità in $NK^\pm$.
  • A differenza degli approcci precedenti, questa dimostrazione gestisce l'intero linguaggio proposizionale (incluso $\lor$) e si basa su risorse matematiche elementari, evitando l'induzione su barra o i modelli canonici.

5. Significato e Rivendicazioni
Il saggio sostiene di fornire una nuova semantica proof-theoretic per la logica classica che:

1. Unifica IPL e CPL: Dimostra che la logica classica può essere compresa come logica intuizionista integrata da un principio primitivo di dualità a livello atomico.
2. Rispetta l'Anti-Realismo: Evitando i valori di verità e la bivalenza, e utilizzando una dimostrazione di completezza costruttiva, offre una fondazione genuinamente anti-realista per la logica classica, affrontando la sfida fondazionale di Dummett.
3. Semplifica la Complessità Tecnica: Limitando il bilateralismo ai letterali e trattando le formule complesse come strutturali, gli autori ottengono una dimostrazione di completezza di "carattere sorprendentemente elementare" paragonabile al lavoro di Sandqvist sulla logica intuizionista, superando le difficoltà tecniche dei precedenti tentativi di B-eS classica.
4. Offre un'Alternativa alla Model Theory: Gli autori posizionano questo lavoro come un'alternativa alla semantica model-theoretic e agli esistenti approcci P-tS che si basano su concetti model-theoretic (come quelli di Makinson o Eckhardt e Pym), mirando a stabilire un conto puramente inferenzialista della logica classica.

Il saggio conclude che questo quadro apre la possibilità di un trattamento sistematico delle logiche classiche analogamente al trattamento sistematico già stabilito per le logiche intuizioniste all'interno della tradizione P-tS.