Logica lineare
# 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. 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 e la linguistica, 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:

| ::= | $p$ ∣ $p$$^⊥$ |
| - | - |
| ∣ | $A$ ⊗ $A$ ∣ $A$ ⊕ $A$ |
| ∣ | $A$ & $A$ ∣ $A$ ⅋ $A$ |
| ∣ | 1 ∣ 0 ∣ ⊤ ∣ ⊥ |
| ∣ | !$A$ ∣ ?$A$ |

dove $p$ e $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 $A$ in CLL ha un suo duale $A$$^⊥,$ definito come segue:

| $(p)$$^⊥$$=p$$^⊥$ | $(p)$$^⊥$$=p$$^⊥$ | $(p)$$^⊥$$=p$$^⊥$ | $(p$$^⊥$$)$$^⊥$ $=p$ | $(p$$^⊥$$)$$^⊥$ $=p$ | $(p$$^⊥$$)$$^⊥$ $=p$ |
| - | - | - | - | - | - |
| $(A$ ⊗ $B$$)^⊥$$=A$$^⊥$ ⅋ $B$$^⊥$ | $(A$ ⊗ $B$$)^⊥$$=A$$^⊥$ ⅋ $B$$^⊥$ | $(A$ ⊗ $B$$)^⊥$$=A$$^⊥$ ⅋ $B$$^⊥$ | ($A$ ⅋ $B$$)^⊥$$=A$$^⊥$ ⊗ $B$$^⊥$ | ($A$ ⅋ $B$$)^⊥$$=A$$^⊥$ ⊗ $B$$^⊥$ | ($A$ ⅋ $B$$)^⊥$$=A$$^⊥$ ⊗ $B$$^⊥$ |
| $A$ ⊕ $B$$)^⊥$$=A$$^⊥$ & $B$$^⊥$ | $A$ ⊕ $B$$)^⊥$$=A$$^⊥$ & $B$$^⊥$ | $A$ ⊕ $B$$)^⊥$$=A$$^⊥$ & $B$$^⊥$ | $(A$ & $B$$)^⊥$$=A$$^⊥$ ⊕ $B$$^⊥$ | $(A$ & $B$$)^⊥$$=A$$^⊥$ ⊕ $B$$^⊥$ | $(A$ & $B$$)^⊥$$=A$$^⊥$ ⊕ $B$$^⊥$ |
| $(1)$$^⊥$$=$⊥ | $(1)$$^⊥$$=$⊥ | $(1)$$^⊥$$=$⊥ | $(⊥)^⊥$$=1$ | $(⊥)^⊥$$=1$ | $(⊥)^⊥$$=1$ |
| $(0)$$^⊥$$=$⊤ | $(0)$$^⊥$$=$⊤ | $(0)$$^⊥$$=$⊤ | $(⊤)^⊥$$=0$ | $(⊤)^⊥$$=0$ | $(⊤)^⊥$$=0$ |
| $(!A)$$^⊥$$=?(A$$^⊥$$)$ | $(!A)$$^⊥$$=?(A$$^⊥$$)$ | $(!A)$$^⊥$$=?(A$$^⊥$$)$ | $(?A)$$^⊥$$=!(A$$^⊥$$)$ | $(?A)$$^⊥$$=!(A$$^⊥$$)$ | $(?A)$$^⊥$$=!(A$$^⊥$$)$ |

Classificazione dei connettivi :

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

Si osservi che $(-)$$^⊥$ è un'involuzione, ossia per qualsiasi proposizione $A$$^{⊥⊥}$$=A$. $A$$^⊥$ è anche detta negazione lineare di $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 $A$⊸$B:=A$$^⊥⅋$$B$. Il connettivo ⊸ è talvolta chiamato "lollipop" a causa della sua forma.

