Sintesi Tecnica: Semantica dell'Inferenza-Comportamento per tutti i connettivi $\text{All}^*$ nei Calcoli Sequentziali Bidimensionali

1. Definizione del Problema

Il saggio affronta una sfida centrale nella Semantica della Teoria della Dimostrazione (P-tS): come fornire spiegazioni semantiche invarianti rispetto al significato per i connettivi logici attraverso diversi sistemi logici (ad esempio, logiche classica, intuizionistica, lineare e dual-intuizionistica). Gli approcci tradizionali, come la Semantica Modello-Teoretica (M-tS) e la Semantica Base-Extension (B-eS), soffrono spesso di "globalismo", dove il cambiamento della logica necessita di un cambiamento del significato dei connettivi (ad esempio, la "congiunzione" classica rispetto alla "congiunzione" intuizionistica). Ciò conduce a una situazione in cui i disaccordi logici vengono ridotti a meri malintesi comunicativi dovuti a diverse definizioni, piuttosto che a disaccordi sostanziali su concetti condivisi.

Il problema specifico che questo saggio affronta è la mancanza di un'implementazione sistematica e formale della Semantica dell'Inferenza-Comportamento (I-bS), un recente approccio proposto da Nagler [Nag26]. Sebbene l'I-bS offra un quadro promettente per isolare il "comportamento inferenziale minimo" di un connettivo per definirne il significato, esso mancava precedentemente di una valutazione tecnica completa attraverso lo spazio di tutti i possibili regole di connettivi. Il saggio mira a validare l'I-bS applicandolo a un vasto insieme non strutturato di connettivi candidati per determinare quali, se non tutti, possiedano significati minimi distinti indipendentemente dalle specifiche regole strutturali (come l'attenuazione o la contrazione).

2. Metodologia

Lo studio impiega un approccio rigoroso e basato sui dati per misurare il "significato" dei connettivi in base al loro uso inferenziale in un contesto minimo.

2.1 Oggetto di Indagine: Tutti i connettivi $\text{All}^*$

Gli autori definiscono l'ambito di indagine come tutti i connettivi $\text{All}^*$: coppie di regole operative formulabili in calcoli sequentziali bidimensionali soggetti alle seguenti restrizioni:

• Regole Operative: Devono essere separate, esplicite e simmetriche (Definizione 3).
• Vincoli: Al massimo due sequenti di premesse e al massimo due formule attive per regola.
• Spazio Totale: Ciò produce esattamente 10.816 coppie di regole sintatticamente uniche (combinazioni di forme di premesse e posizioni di formule attive).

2.2 Ambiente di Test: Relazione di Derivabilità Minima

Per isolare il significato di un connettivo dalle caratteristiche strutturali di logiche specifiche, gli autori utilizzano un calcolo di base minimale costituito da:

• Identità ($Id_{pr}$): Limitata a formule primitive soltanto.
• Taglio ($Cut_{cd}$): Una regola di Taglio che differenzia i contesti.
• Assunzioni Strutturali: Il calcolo assume lo Scambio (multisetti) ma esclude l'Attenuazione (Weakening) e la Contrazione. Questo rappresenta il "nucleo substrutturale" comune a molte logiche.

2.3 Dispositivo di Misura: Comportamento Inferenziale

La metrica centrale è il comportamento inferenziale, definito come il pattern sintattico che un connettivo esibisce quando la sua definibilità viene provata all'interno del calcolo minimale.

• Criteri di Definibilità: Seguendo Belnap [Bel62], un connettivo è definibile se la sua aggiunta al calcolo risulta in un'estensione conservativa (nessun nuovo teorema senza il connettivo) e in unicità (il connettivo è unicamente determinato fino all'isomorfismo).
• Clausola Semantica: Il "significato" di un connettivo è identificato come la sua coppia di regole operative minima che produce il profilo di comportamento inferenziale minimo (la lista più breve di posizioni di componenti occupate dal connettivo e dalle sue formule attive durante una prova di definibilità).

2.4 Generazione e Analisi dei Dati

Gli autori filtrano sistematicamente i 10.816 candidati:

1. Filtro 1 (Formulabilità): Tutte le 10.816 coppie di regole.
2. Filtro 2 (Conservatività): Dimostrare l'eliminazione del Taglio per i casi positivi e costruire controesempi per quelli non conservativi. Questo riduce l'insieme a 376 connettivi conservativi.
3. Filtro 3 (Unicità): Stabilire l'interderivabilità orizzontale e verticale. Questo riduce ulteriormente l'insieme a 150 connettivi unicamente definibili.
4. Analisi della Minimalità: Tra i 150 connettivi definibili, gli autori distinguono tra connettivi "minimali" e "bloatnectives" (connettivi equivalenti con ridondanze sintattiche). Applicando criteri di minimalità del tipo di premessa (cardinalità più bassa di sequenti di premesse), isolano le clausole semantiche realmente minime.

3. Contributi Chiave e Risultati

3.1 Identificazione di 21 Connettivi Minimalmente Significativi

Il risultato primario è l'identificazione di esattamente 21 connettivi minimamente significativi. Questi corrispondono a costanti logiche familiari e ai loro conversi/inversi, ma con distinzioni precise tra versioni additive (lattice) e multiplicative (gruppo):

• Nullari: Falso ($\bot$) e Vero ($\top$).
• Unari: Due forme di negazione (Intuizionistica $\neg$ e Dual-Intuizionistica $\sim$), e una negazione inversa "triviale".
• Binari:
  • Congiunzione: Additiva ($\sqcap$) e Moltiplicativa ($\otimes$).
  • Disgiunzione: Additiva ($\sqcup$) e Moltiplicativa ($\oplus$).
  • Implicazione: Additiva Destra ($\rightsquigarrow$), Moltiplicativa Destra ($\to$), Additiva Sinistra e Moltiplicativa Sinistra.
  • Conversi e Inversi: Ognuno dei sopra citati ha clausole semantiche distinte per i propri conversi (scambio di componenti) e inversi.

3.2 Clausole Semantiche e Framework

Il saggio fornisce clausole semantiche esplicite (coppie di regole minime) per ciascuno dei 21 connettivi. Fondamentalmente, dimostra che questi significati sono indipendenti dalla logica. Ad esempio, la clausola semantica per la congiunzione moltiplicativa ($\otimes$) è la stessa sia che appaia nella Logica Lineare, nella Logica Classica o nella Logica Intuizionistica. Le differenze nel modo in cui questi connettivi si comportano nelle logiche complete (ad esempio, l'equivalenza tra $\otimes$ e $\sqınd$ nella Logica Classica) sono attribuite alle risorse strutturali (come Contrazione e Attenuazione) piuttosto che a un cambiamento nel significato centrale del connettivo.

3.3 Interrelazioni Semantiche tra le Logiche

Lo studio mappa la compatibilità semantica di questi 21 connettivi attraverso varie logiche:

• Logica Classica (LK): Confluisce le versioni additive e multiplicative di congiunzione, disgiunzione e implicazione. Confluisce inoltre le due forme di negazione.
• Logica Intuizionistica (LJ): È compatibile con le versioni additive di congiunzione e disgiunzione, e con l'implicazione "destra", ma cattura solo metà del significato della negazione classica (specificamente $\neg_{min}$, escludendo $\sim_{min}$).
• Logica Dual-Intuizionistica (LDJ): Cattura l'altra metà della negazione classica ($\sim_{min}$) e i duali degli altri connettivi.
• Logica Lineare (LL): Distingue tutti i 21 connettivi, trattandoli come semanticamente distinti.

3.4 Validazione di I-bS

Il saggio sostiene di validare il framework della Semantica dell'Inferenza-Comportamento dimostrando che, quando applicata a una ricerca cieca ed esaustiva di possibili regole senza pregiudizi verso una logica specifica, la teoria converge naturalmente sugli esatti connettivi standard trovati nei sistemi logici stabiliti. Il fatto che il "rumore" (le altre 10.795 coppie di regole) venga filtrato come non definibile o non minimale funge da "controllo di sanità" (sanity check) per la teoria.

4. Significato e Rivendicazioni

Il saggio posiziona i suoi risultati come una verifica del framework della Semantica dell'Inferenza-Comportamento. La sua importanza risiede in:

1. Indipendenza dalla Logica: Fornisce un metodo per definire i significati dei connettivi che sono invarianti attraverso diverse logiche. Cambiare la logica (ad esempio, aggiungere l'Attenuazione) non cambia il significato del connettivo; cambia solo il contesto strutturale in cui il connettivo opera.
2. Risoluzione del Cambiamento di Significato: Offre una spiegazione semantica del perché le logiche classica e intuizionistica sembrano dissentire. Esse non dissentono necessariamente sul significato di "e" o "o"; piuttosto, differiscono su quali connettivi minimi permettono di interagire e quali regole strutturali permettono. Ad esempio, la "e" classica è una confluenza di due distinti significati minimi ($\otimes$ e $\sqcap$), mentre la "e" intuizionistica è strettamente $\sqcap$.
3. Parsimonia Ontologica: L'approccio non richiede modelli o basi esterne, affidandosi esclusivamente al nucleo substrutturale del sistema di dimostrazione.
4. Esaustività: Coprendo l'intero spazio di regole formulabili sotto i dati vincoli, il saggio rivendica di aver fornito una tassonomia completa dei significati minimi dei connettivi nei calcoli sequentziali bidimensionali.

Gli autori rimangono modesti riguardo all'estensione, osservando che i risultati sono relativi ai vincoli specifici (due premesse, due formule attive, calcolo minimale specifico) e che lavori futuri potrebbero esplorare calcoli multidimensionali, la quantificazione o relazioni di derivabilità minima alternative. Tuttavia, entro il perimetro definito, il saggio afferma che l'I-bS riesce a isolare i significati primitivi dei connettivi logici.