Logica lineare

La logica lineare è una logica substrutturale proposta da Jean-Yves Girard come un raffinamento della logica classica ed intuizionista, coniugando le dualità che caratterizzano i connettivi della prima con le proprietà costruttive della seconda^[1]. Sebbene questo sistema logico sia un oggetto di studio fine a sé stesso, più in generale le idee della logica lineare hanno influito in settori come i linguaggi di programmazione, la game semantics o la fisica dei quanti^[2] e la linguistica^[3], in particolare per la sua enfasi sulle risorse limitate, la dualità e l'interazione.

La logica lineare, di per sé, si presta a molteplici presentazioni e spiegazioni. Dal punto di vista della teoria della dimostrazione deriva da un'analisi del calcolo dei sequenti classico in cui gli usi della regola di contrazione e di indebolimento (regole strutturali) sono attentamente regolati. Al livello operativo questo significa che la deduzione logica non riguarda più solo l'espandere un insieme di "proposizioni vere", ma è anche un modo per manipolare risorse che non possono essere sempre duplicate o eliminate a piacere. In termini di semplici modelli denotazionali, la logica lineare può essere considerata come un raffinamento dell'interpretazione della logica intuizionistica sostituendo le categorie cartesiane chiuse con categorie monoidali simmetriche, o dell'interpretazione della logica classica sostituendo le algebre booleane con le C*-algebre.

Sintassi

Il linguaggio della logica lineare classica (CLL) è definito induttivamente dalla seguente BNF:

${\displaystyle A}$	::=	${\displaystyle p}$ ∣ ${\displaystyle p}$⊥
	∣	${\displaystyle A}$ ⊗ ${\displaystyle A}$ ∣ ${\displaystyle A}$ ⊕ ${\displaystyle A}$
	∣	${\displaystyle A}$ & ${\displaystyle A}$ ∣ ${\displaystyle A}$ ⅋ ${\displaystyle A}$
	∣	1 ∣ 0 ∣ ⊤ ∣ ⊥
	∣	!${\displaystyle A}$ ∣ ?${\displaystyle A}$

dove ${\displaystyle p}$ e ${\displaystyle p}$^⊥ appartengono all'insieme delle proposizioni atomiche del linguaggio. Per motivi che saranno spiegati in seguito, i connettivi ⊗, ⅋, 1 e ⊥ sono detti moltiplicativi, mentre &, ⊕, ⊤ e 0 additivi, e i connettivi ! e ? sono chiamati esponenziali. In più, possiamo impiegare la seguente terminologia:

• ⊗ è detto "congiunzione moltiplicativa" o "per" (talvolta anche "tensore")
• ⊕ è detto "disgiunzione additiva" o "più"
• & è detto "congiunzione additiva" o "con"
• ⅋ è detto "disgiunzione moltiplicativa" o "par"
•  ! si legge "certamente" (o "bang")
•  ? si legge "perché no"

Ogni proposizione ${\displaystyle A}$ in CLL ha un suo duale ${\displaystyle A}$^⊥, definito come segue:

${\displaystyle (p)}$⊥${\displaystyle =p}$⊥			${\displaystyle (p}$⊥${\displaystyle )}$⊥ ${\displaystyle =p}$
${\displaystyle (A}$ ⊗ ${\displaystyle B}$)⊥${\displaystyle =A}$⊥ ⅋ ${\displaystyle B}$⊥			(${\displaystyle A}$ ⅋ ${\displaystyle B}$)⊥${\displaystyle =A}$⊥ ⊗ ${\displaystyle B}$⊥
${\displaystyle A}$ ⊕ ${\displaystyle B}$)⊥${\displaystyle =A}$⊥ & ${\displaystyle B}$⊥			${\displaystyle (A}$ & ${\displaystyle B}$)⊥${\displaystyle =A}$⊥ ⊕ ${\displaystyle B}$⊥
${\displaystyle (1)}$⊥${\displaystyle =}$⊥			(⊥)⊥${\displaystyle =1}$
${\displaystyle (0)}$⊥${\displaystyle =}$⊤			(⊤)⊥${\displaystyle =0}$
${\displaystyle (!A)}$⊥${\displaystyle =?(A}$⊥${\displaystyle )}$			${\displaystyle (?A)}$⊥${\displaystyle =!(A}$⊥${\displaystyle )}$

Classificazione dei connettivi

	add	mul	exp
pos	⊕ 0	⊗ 1	!
neg	& ⊤	⅋ ⊥	?

Si osservi che ${\displaystyle (-)}$^⊥ è un'involuzione, ossia per qualsiasi proposizione ${\displaystyle A}$^⊥⊥${\displaystyle =A}$. ${\displaystyle A}$^⊥ è anche detta negazione lineare di ${\displaystyle A}$.

Le colonne della tabella suggeriscono un altro modo per classificare i connettivi della logica lineare, chiamato polarità: i connettivi negati nella colonna di sinistra (⊗, ⊕, 1, 0,!) sono chiamati positivi, mentre i loro duali a destra (⅋, &, ⊥, ⊤,?) sono chiamati negativi; cf. tabella a destra.

L'implicazione lineare non è inclusa nella grammatica dei connettivi, ma è definibile nella CLL usando la negazione lineare e la disigunzione moltiplicativa (par), da ${\displaystyle A}$⊸${\displaystyle B:=A}$^⊥⅋${\displaystyle B}$. Il connettivo ⊸ è talvolta chiamato "lollipop" a causa della sua forma.