Una semantica per la logica lineare

 5 
La classe delle funzioni stabili che va da uno spazio coerente ad un altro è isomorfa ad 
uno spazio coerente, quindi è elemento del dominio delle funzioni stabili. Questo ci 
permette di poter riscrivere i connettivi logici sotto forma di funzioni stabili da spazi 
coerenti a spazi coerenti, cioè di avere una immagine costrutt iva della logica 
intuizionista nel senso di Heyting
1
. 
La logica lineare nacque, per così dire, quando Girard mise l'accento sul fatto che le 
funzioni stabili che rappresentano i connettivi della logica intuizionista possono essere 
ottenute come composizione di un'altra classe di funzioni, le funzioni lineari. La classe 
delle funzioni lineari è un sottoinsieme della classe delle funzioni stabili, quindi per essa 
vale tutto ciò che vale per le funzioni stabili, ma la peculiarità delle funzioni lineari è 
che esse tengono maggiormente in conto la quantità e la molteplicità nel passare 
dall'insieme argomento all'insieme valore. Ciò significa che da un punto di vista 
sintattico si è potuto ottenere una logica i cui connettivi corrispondono alle funzioni 
lineari della semantica delle dimostrazione basata sugli spazi coerenti. 
A noi in questa sede non interessa entrare nello specifico della semantica della 
dimostrazione per la logica lineare, quello che ci interessa è porre l'accento su alcune 
caratteristiche della logica suddetta che derivano direttamente dal contesto in cui è nata. 
In particolare mettiamo in rilievo che  
 
1) La logica lineare, in quanto nasce già fornita di una semantica della 
dimostrazione, quella basata sugli spazi coerenti e sulle funzioni lineari, 
è una logica costruttiva nello stesso senso in cui lo è la logica 
intuizionista. 
 
2) Pur essendo costruttiva, la logica lineare ci permette di abbandonare 
l'ipotesi limitativa fatta da Hey ting e cioè che le dimostrazioni di una 
logica costruttiva debbano avere una sola conclusione, infatti alle virgole 
tra le assunzioni corrisponde una operazione tra spazi coerenti ed alle 
virgole tra le conclusioni ne corrisponde un'altra. Questo è un risultato 
interessante per l'ut ilizzo informatico della logica lineare. 
 
                                                 
1
 Si rimanda a [2] per una presentazione chiara ed estesa di quanto accennato sopra.  
 6 
3) Dalle peculiarità delle funzioni lineari rispetto a quelle stabili deriva che 
la logica lineare è una logica sensibile alle risorse, cioè non è indifferente 
il numero delle volte che una assunzione viene usata, oppure una 
conclusione ottenuta, in una dimostrazione. 
 
Per la formulazione sintattica della logica lineare, Girard usò il calcolo dei sequenti 
che è rimasto nella letteratura lo strumento sintattico privilegiato per il suo studio. 
Il calcolo dei sequenti, infatti, mette in evidenza sintatticamente quelle che sono, sul 
versante della semantica della dimostrazione, le peculiarità delle funzioni lineari rispetto 
alle funzioni stabili. Da un punto di vista formale, tali peculiarità si traducono con 
l'eliminazione delle due regole strutturali di indebolimento e contrazione. 
L'eliminazione delle due regole suddette ci obbliga a non trascurare il numero delle 
volte che un'assunzione viene usata ed una conclusione ottenuta e quindi riproduce la 
"sensibilità" alla quantità e alla moltep licità delle funzioni lineari. Vedremo in seguito 
più in dettaglio come ciò avvenga. 
 
 
 
2. La logica lineare: una logica substrutturale. 
Abbiamo ritenuto opportuno accennare alla storia della logica lineare e quindi alla sua 
semantica della dimostrazione per rendere più comprensibile la natura dello strumento, 
se non altro adesso si comprende perché questa logica sia detta "lineare", tuttavia, nella 
trattazione che seguirà, la logica lineare viene introdotta in maniera squisitamente 
sintatt ica. Questo approccio riflet te completamente quello della letteratura che tende a 
liberare tutte le potenzialità dello strumento svincolandolo dall'alveo d'origine. 
In questo lavoro la logica lineare verrà introdotta e trattata come una logica 
substrutturale. Le logiche substrutturali sono quelle logiche che si ottengono a partire 
dai calcoli dei sequenti di Gentzen, LK o LJ (rispettivamente per la logica classica o per 
la logica intuizionista), con la soppressione di alcune o tutte le regole strutturali ed 
adeguati aggiustamenti tecnici. 
Partendo dalle caratteristiche sintattiche di CLL, calcolo dei sequenti per la logica 
lineare classica, cercheremo di comprendere il senso ep istemologico delle differenze 
tecniche che intercorrono tra LK e CLL. In un secondo momento metteremo in evidenza 
 7 
le proprietà sintattiche di CLL e poi provvederemo a descrivere una semantica della 
verità che interp reti adeguatamente CLL. 
 8 
I. CLL: calcolo dei sequenti per la logica lineare classica 
 
 
 
 
 
1. Premessa 
Da un punto di vista tecnico CLL (Logica lineare classica) si ottiene dal Calcolo dei 
Sequenti per la Logica Classica (LK) ideato da Gentzen con le seguenti modifiche 
i) Eliminazione delle regole strutturali di indebolimento e contrazione sia a 
destra che a sinistra (continua a valere la regola di scambio); 
ii) Sdoppiamento di alcuni connettivi logici per causa diretta di (i); 
iii) Definizione di due operatori logici che reintroducono per formule 
specifiche l'indebolimento e la contrazione. 
Queste variazioni tecniche tra LK e CLL hanno implicazioni teoriche estremamente 
interessanti. Del resto anche mettendo a confronto LK con LJ è evidente come piccole 
differenze tecniche
2
 tra sistemi formali nascondano concezioni epistemologiche 
estremamente diverse. Vediamo ora p iù p recisamente cosa accade con l'eliminazione in 
LK delle due regole strutturali. 
 
 
 
2. Contrazione e indebolimento 
Cerchiamo innanzitutto di comprendere il senso della contrazione e dell'indebolimento 
in LK e che cosa implica la loro soppressione. 
La regola di contrazione a sinistra in LK,  
∆⇒Γ
∆⇒Γ
,
,,
α
αα
 (dove α  è una formula di LK, Γ  e ∆  sono 
successioni finite di formule di LK e ⇒  è il 
simbolo di sequente) 
                                                 
2
 Ricordiamo che LJ è una restrizione di LK, cioè si impone che a destra del simbolo di sequente ci sia al 
massimo una formula e si adeguano le regole di LK a questo vincolo. 
 9 
permette di tralasciare il numero delle volte che un'assunzione è stata usata in una 
derivazione, mentre la contrazione a destra, 
  
α
αα
,
,,
∆⇒Γ
∆⇒Γ
 
permette di tralasciare il numero delle volte che una conclusione è stata ottenuta in una 
derivazione. 
La regola di indebolimento a sinistra, 
∆⇒Γ
∆⇒Γ
,α
 
afferma che una proposizione è un'assunzione di una deduzione anche se non è stata 
usata nel corso di tale derivazione e l'indebolimento a destra 
α,∆⇒Γ
∆⇒Γ
 
afferma che una proposizione è una conclusione di una derivazione anche se non è 
stata ottenuta nella suddetta derivazione. 
Queste due regole prese nel loro insieme ci permettono di non preoccuparci del 
numero delle volte che un'assunzione è usata in una derivazione e del numero delle 
volte che una conclusione è ottenuta in una derivazione. Ciò è del tutto lecito se si tiene 
p resente che l'oggetto d'indagine della logica classica e della logica intuizionista, di cui 
LK e LJ sono due formalizzazioni, è il ragionamento matematico. Nei ragionamenti 
matematici è del tutto naturale ignorare il numero delle volte che un'assunzione o una 
conclusione compare in una derivazione: nessun matematico affermerebbe che ha usato 
quattro volte l'ipotesi o l'assunzione α  per dimostrare due volte la conclusione β . 
In CLL, però, l'eliminazione delle due regole strutturali analizzate sopra ci impone di 
non potere più ignorare il numero delle volte che un'assunzione è usata o una 
conclusione ottenuta in una deduzione, cioè la nostra logica diventa sensibile a quante 
volte una formula compare come assunzione (nell'antecedente) o come conclusione (nel 
conseguente) in un sequente. Anche se questa sembra una finezza superflua in ambito 
matematico, in altri ambiti ci permette di catturare situazioni per cui la logica classica e 
intuizionista sono del tutto inadeguate: ad esempio un chimico non direbbe mai che da 
un numero imprecisato di molecole di tipo α  e da un numero imprecisato di molecole 
di tipo β  si ottiene un numero imprecisato di molecole di tipo δ , in questa situazione è 
 10 
fondamentale conoscere il numero esatto delle formule/molecole dello stesso tipo usate 
nella deduzione/reazione. 
Più in generale, l'eliminazione delle regole strutturali di contrazione ed indebolimento 
e la conseguente cura che viene posta al numero delle volte che una formula compare a 
destra o a sinistra del simbolo di sequente ci permette di concepire le formule non come 
verità stabili, ma come risorse e l'imp licazione logica non come il collegamento tra due 
verità, ma il fatto che attraverso l'utilizzo di una risorsa si riesca a produrne un'altra. 
La logica lineare può essere considerata come una logica "sensibile alle risorse", e da 
questo punto di vista si contrappone sia alla logica intuizionista che alla logica classica. 
Le formule rappresentano tipi di risorse di cui non si può fare un uso infinito. Tratta di 
come si fa a trasformare alcuni tip i di risorse (p remesse) in altre (conclusioni) e deve 
tener conto del numero delle volte in cui una risorsa è usata. In CLL la lettura intuitiva 
di un sequente 
mn
ββαα ,...,,...,
11
⇒  è: "usando una sola volta (consumando) ciascuna 
delle risorse 
i
α  si ott iene una sola volta (si costruisce) ciascuna delle risorse 
i
β ". Le 
regole di CLL ci permettono di passare da sequenti veri sotto questa lettura a sequenti 
veri sotto questa lettura. 
 
Abbiamo visto finora come la caduta della contrazione e indebolimento abbia p rodotto 
una logica sensibile alle risorse, vediamo ora con un esempio come una logica sensibile 
alle risorse sia incompatibile con le due regole strutturali in questione. 
 
ESEM PIO 1. 
Consideriamo le seguenti risorse: =α "5000 lire" =β "un pacchetto di sigarette". 
Se è vero, secondo la suddetta lettura, βα ⇒  (consumando 5.000 lire ottengo un 
pacchetto di sigarette)
3
 allora è vero 
S)  ββαα ,, ⇒  (consumando 10.000 lire ottengo due pacchett i di sigarette) 
cioè 
S)  "5000 lire" , "5000 lire" ⇒ "un pacchetto di sigarette" , "un pacchetto di 
sigarette" 
 
                                                 
3
 Nell'esempio 1 stiamo supponendo che un pacchetto di sigarette costi esattamente 5000 lire. 
 11 
E' subito evidente che se il sequente S è vero secondo la lettura considerata, le regole 
strutturali di indebolimento e di contrazione produrrebbero sequenti falsi sotto questa 
lettura: 
La contrazione a sinistra (così come l'indebolimento a destra) p rodurrebbe una penuria 
di risorse nell'antecedente per poter costituire le risorse del conseguente; 
La contrazione a destra (così come l'indebolimento a sinistra) p rodurrebbe un eccesso 
di risorse nell'antecedente che è ugualmente incompatibile con la nostra lettura di 
sequente. 
 
Questa "concezione dei sequenti"
4
 e la conseguente caduta delle due regole strutturali 
permette alla logica lineare di prestare attenzione ad aspetti completamente "non 
percep it i" dalla logica classica (e intuizionista). E' questo il motivo per cui la logica 
lineare si considera essere un "raffinamento" della logica classica. In realtà la logica 
lineare oltre ad essere un raffinamento della logica classica ne conserva la stessa 
potenza dimostrativa, cioè dimostra tutto ciò che dimostra la logica classica. Con ciò 
intendiamo che esiste una procedura di trascrizione tra il linguaggio di LK e quello di 
CLL tale che un sequente S è dimostrabile in LK se e solo se la sua traduzione S' è 
dimostrabile in CLL. Per approfondimenti su questo punto si rimanda a [10] pagg. 45-
55. 
Ora scendiamo nei dettagli e andiamo a vedere come siano state coniugate le due 
esigenze apparentemente contrapposte di arricchimento espressivo da una parte e 
conservazione della potenza dimostrativa dall'altra. 
 
 
 
3. Connettivi classici e connettivi l ineari 
In questo paragrafo descriveremo i connettevi di CLL raffrontandoli con quelli di LK 
ed in particolare mostreremo come lo sdoppiamento di alcuni connettivi e delle costanti 
in CLL sia strettamente legato alla caduta dell'indebolimento e della contrazione. 
 
Congiunzioni lineari 
                                                 
4
 Abrusci in [1]. 
 12 
Consideriamo le regole per la congiunzione in LK e vediamo che esistono due modi 
equivalenti per definire lo stesso connettivo. Siano α , β  formule qualsiasi; Γ  e ∆  
successioni finite di formule e "E" il simbolo per la congiunzione in LK; definiamo due 
regole per E: 
 
E1 sx
∆⇒Γ
∆⇒Γ
,E
,
βα
α
 e 
∆⇒Γ
∆⇒Γ
,E
,
βα
β
   E1 dx
βα
βα
E,
,     ,
∆⇒Γ
∆⇒Γ∆⇒Γ
 
 
E2 sx
∆⇒Γ
∆⇒Γ
,E
,,
βα
βα
   E2 dx
βα
βα
E,,,
,     ,
∆′∆⇒Γ′Γ
∆′⇒Γ′∆⇒Γ
 
 
Dimostriamo che in LK E1 sx è equivalente ad E2 sx. 
 
E2 sx implica E1 sx: 
Da uno dei due sequenti superiori di E1 Sx, ∆Γ⇒⇒,α , si ottiene 
sx ind.
sx E2
,E
,,
(ip.) ,
∆Γ
∆Γ
∆Γ
⇒
⇒
⇒
βα
βα
α
 
 
E1 sx implica E2 sx: 
Si parte dal sequente superiore di E2 sx 
sx E1
sx E1
sx contraz.
 ,E
,E,E
 ,,E
 (ip.) ,,
∆Γ
∆Γ
∆Γ
∆Γ
⇒
⇒
⇒
⇒
βα
βαβα
ββα
βα
 
 
Dimostriamo ora che  in LK E1 dx è equivalente ad E2 dx. 
 
E1 dx implica E2 dx: 
Si parte dai sequenti superiori di E2 dx 
dx E1
 E,,,
voltedx esx   ind.
  ,,,
,
         voltedx esx   ind.
  ,,,
,
βα
β
β
α
α
∆∆ΓΓ
∆∆ΓΓ
∆Γ
∆∆ΓΓ
∆Γ
′′′⇒′′′
+
′′′
⇒
′′′
′′′
⇒
′′′
+
′′′
⇒
′′′
⇒
 
 
 13 
E2 dx implica E1 dx: 
Dai sequenti superiori di E1 dx si ha 
dx E2
sx edx  contr.
E,
 E,,
,     ,
βα
βα
βα
∆Γ
∆∆ΓΓ
∆Γ∆Γ
⇒
⇒
⇒⇒
 
 
Abbiamo mostrato che in LK E1 è equivalente ad E2 e la dimostrazione poggia 
consistentemente sulle regole strutturali di contrazione ed indebolimento. M a queste 
regole in CLL non ci sono, perciò in CLL E1 ed E2 non sono più due formulazioni 
diverse della stessa regola, ma sono due regole diverse, in quanto non sono equivalenti. 
Per ottenere estensionalmente ciò che era ottenuto da "E" in LK, in CLL abbiamo 
bisogno di due connettivi: " ⊗ " per la definizione moltip licativa (E2) e " ∧ " per la 
definizione additiva (E1), dove "additivo" e "moltiplicativo" sono aggettivi che si 
riferiscono a caratteristiche semantiche delle funzioni corrispondenti. 
 
Disgiunzioni lineari 
Analogamente alle congiunzioni, la disgiunzione di LK si divide in CLL in due 
connettivi ben distinti, ed anche in questo caso il motivo della non equivalenza tra i due 
connettivi è l'assenza delle regole strutturali. I simboli dei due connettivi sono ⊕  e ∨ . 
⊕  è il duale di ⊗  rispetto alla copp ia assunzioni/conclusioni: ⊕  si comporta a sinistra 
del simbolo di sequente come ⊗  si comporta a destra e si comporta a destra come ⊗  si 
comporta a sinstra. ∨  è il duale di ∧ . In CLL le regole sono: 
 
∨  sx
∆⇒Γ∨
∆⇒Γ∆⇒Γ
,
,     ,
βα
βα
   ∨  dx (
βα
α
∨∆⇒Γ
∆⇒Γ
,
,
 e 
βα
β
∨∆⇒Γ
∆⇒Γ
,
,
) 
 
⊕  sx
∆′∆⇒Γ′Γ⊕
∆′⇒Γ′∆⇒Γ
,,,
,     ,
βα
βα
   ⊕  dx
βα
βα
⊕∆⇒Γ
∆⇒Γ
,
,,
 
 
Dimostriamo che in LK i due connetivi sono intercambiabili, cioè indicano la stessa 
entità logica. 
Dalle premesse di ⊕  sx si ottiene: 
 14 
sx  
,,,
sx  edx  ind.
 ,,,
,
sx      edx  ind. 
,,,
,
∨
′′′⇒′′′∨
′′′
⇒
′′′
′′′
⇒
′′′
′′′
⇒
′′′
⇒
∆∆ΓΓ
∆∆ΓΓ
∆Γ
∆∆ΓΓ
∆Γ
βα
β
β
α
α
 
 
Dalle premesse di ∨  sx si ottiene: 
sx 
sx edx  contr.
,
,,,
,     ,
⊕
⇒⊕
⇒⊕
⇒⇒
∆Γ
∆∆ΓΓ
∆Γ∆Γ
βα
βα
βα
 
 
Dalle premesse di ⊕  dx si ha: 
dx 
dx contr.
 ,
 ,,
dx 
 ,,
,,
∨
∨⇒
∨∨⇒
∨
∨⇒
⇒
βα
βαβα
ββα
βα
∆Γ
∆Γ
∆Γ
∆Γ
 
 
Da una delle due premesse di ∨  dx si ha: 
dx 
 ,
dx ind.
 ,,
,
⊕
⊕⇒
⇒
⇒
βα
βα
α
∆Γ
∆Γ
∆Γ
 
 
Da quello che abbiamo mostrato sopra è chiaro che in LK sarebbe del tutto superfluo 
usare due connettivi del tutto intercambiabili, o meglio due simboli dello stesso 
connettivo. In CLL, invece, non esiste nessuna ridondanza, in quanto le due regole 
esprimono entità logiche diverse tra loro. 
 
Costanti proposizionali 
In CLL sono presenti quattro proposizioni costanti, " Τ ", " ⊥ ", "0" e "1". "0" e " ⊥ " 
sono due nomi del falso, mentre "1" e " Τ " sono due nomi del vero. Il motivo per cui 
queste costanti sono quattro invece di due è lo stesso che impone due congiunzioni e 
due disgiunzioni: l'eliminazione della contrazione e dell'indebolimento.  
Le regole (e assiomi) in CLL sono: 
 
0 sx (Ax) ⇒0       0 dx
0,∆⇒Γ
∆⇒Γ
 
 15 
⊥  sx (Ax) ∆⇒Γ⊥ ,     Nessuna regola per ⊥  dx 
 
1 sx
∆⇒Γ
∆⇒Γ
,1
       1 dx (Ax) 1⇒  
Nessuna regola per Τ  sx     Τ  dx (Ax) Τ∆⇒Γ , 
 
In presenza di contrazione ed indebolimento 0 è equivalente a ⊥  e 1 è equivalente a 
Τ . 
M ostriamo che 0 e ⊥  sono intercambiabili in presenza di contrazione ed 
indebolimento. 
Si vede subito che 0 sx e ⊥  sx sono intercambiabili in LK infatt i per ⊥ sx si ha ⇒⊥  
e da 0 sx si ha  
sx eind.dx 
,0
0
∆Γ⇒⇒
⇒
 
 
Per quanto riguarda l'introduzione a destra, per mostrare che 0 e ⊥  sono del tutto 
intercambiabili, da ∆Γ⇒⇒  dobbiamo ottenere ⊥⇒ ,∆Γ . Innanzi tutto anticip iamo che 
in CLL un sequente 
mn
δδγγ ,...,,...,
11
⇒  è equivalente alla formula 
mn
δδγγ ⊕⊕⊃⊗⊗ ,...,,...,
11
, e anche che in CLL si dimostra che ⊥  è l'elemento neutro 
di ∨ , cioè αα ⇔∨⊥  (proposizione 1 par. 5.1). Ora in caso di validità della 
contrazione ed indebolimento si avrebbe che ⊕  è equivalente a ∨  e cioè varrebbe 
αα ⇔⊕⊥ , e quindi  
 
⊥⊕⊕⊕⊃⊗⊗
⊕⊕⊃⊗⊗
mn
mn
δδγγ
δδγγ
,...,,...,
,...,,...,
11
11
 
 
Il che significa che da ∆Γ⇒⇒  si otterrebbe ⊥⇒ ,∆Γ . 
La dimostrazione che 1 e Τ  siano equivalenti in presenza di contrazione ed 
indebolimento è simmetrica alla precedente, si usa che in CLL αα ⇔∧Τ  
(proposizione 1 par. 5.1). 
 
Implicazione lineare 
 16 
L'implicazione lineare è il connettivo fondamentale della logica lineare, è quello che 
storicamente nasce per primo e da cui deriva la concezione lineare dei sequenti. Noi 
useremo il simbolo ⊃  per l'imp licazione lineare. βα ⊃  è equivalente al sequente 
βα ⇒ , indica il fatto che posso ottenere un tipo di risorse β  consumando un tipo di 
risorse α . 
In CLL l'implicazione lineare si definisce in questo modo: 
 
⊃  sx
∆′∆⇒Γ′Γ⊃
∆′⇒Γ′∆⇒Γ
,,,
 ,    ,
βα
βα
   ⊃  dx
βα
βα
⊃∆⇒Γ
∆⇒Γ
,
,,
 
 
Si potrebbe definire, coerentemente a quanto abbiamo fatto per congiunzione, 
disgiunzione e costanti proposizionali, ⊃
′
 tale che: 
 
⊃
′
 sx
∆⇒Γ⊃
∆⇒Γ∆⇒Γ
,
,    ,
βα
βα
   ⊃
′
 dx(
βα
α
⊃∆⇒Γ
∆⇒Γ
,
,
 e 
βα
β
⊃∆⇒Γ
∆⇒Γ
,
,
) 
 
e si può mostrare che ⊃  e ⊃
′
 sono equivalenti in LK e non in CLL, ma in CLL viene 
definita la sola implicazione lineare ⊃  che è sufficiente a garantire, in concerto con gli 
altri operatori lineari, una adeguata potenza dimostrativa. 
 
Negazione 
La negazione " ¬ " in CLL ha il compito di trasformare una proposizione-risorsa nel 
suo duale rispetto alla coppia assunzione/conclusione.  
 
¬  sx
∆⇒Γ¬
∆⇒Γ
,
,
α
α
     ¬  dx
α
α
¬∆⇒Γ
∆⇒Γ
,
,
 
 
Cerchiamo di chiarire quanto appena detto. Quando una formula compare in una 
deduzione nel calcolo dei sequenti è sempre all'interno di un sequente, non ha senso 
pensare in CLL o in LK una formula completamente decontestualizzata. Quindi pensare 
una formula in CLL significa pensarla o come assunzione o come conclusione di un 
sequente ed in nessun altro modo, perciò lo stare a destra o a sinistra del simbolo di 
sequente è un contributo indispensabile al senso della formula stessa.  
 17 
In CLL la negazione non fa altro che invertire il senso di una proposizione, 
spostandola da una parte all'altra del simbolo di sequente. Se =α «ottengo "5000 Lire"» 
allora =¬ α «consumo "5000 Lire"», dove "ottengo" e "consumo" sono i termini che 
esplicitano la posizione della formula. La risorsa è la stessa, ma la negazione scambia 
l'uno nell'altro i due possibili stat i (uno il duale dell'altro) in cui può essere concepita la 
risorsa. 
La cosa importante è che la negazione ha carattere involutivo cioè si comporta come la 
negazione classica. In CLL è dimostrabile, come vedremo in seguito 
αα ¬¬⇔ . 
 
Esponenziali 
La logica ottenuta fino a questo momento, con l'eliminazione della contrazione e 
dell'indebolimento e la suddivisione della congiunzione, disgiunzione e costanti, coglie 
aspetti che la logica classica (e intuizionista) non riesce a cogliere, ma è estremamente 
debole, infatti non è per niente adeguata a situazioni in cui si tratta con verità stabili, in 
cui è indifferente quante volte un'assunzione viene usata o una conclusione ottenuta. Per 
poter catturare anche queste situazioni c'è bisogno di introdurre altri due connettivi i cui 
simboli saranno !, ?. I due connettivi sono l'uno il duale dell'altro, cioè quello che ! fa a 
sinistra ? fa a destra del simbolo di sequente. α!  nelle assunzioni esprime il fatto che la 
risorsa α  viene usata un numero indefinito, ma finito di volte; α?  nelle conclusioni, 
invece esp rime il fatto che la risorsa α  viene costituita un numero indefinito, ma finito 
di volte. Quindi lo scopo di questi due connettivi è, rimanendo fedeli all'ottica della 
cosiddetta sensibilità alle risorse, trattare alcune risorse come immagazzinate in quantità 
ingente tanto da poterle considerare inesauribili per quello che sono i nostri scopi
5
. E' 
proprio in questo modo che la nostra logica può catturare verità stabili: trat tandole come 
risorse di cui si ha una disponibilità arbitraria.  
Da un punto di vista sintattico il nostro scopo è quello di introdurre un certo numero di 
regole che ci permetta di leggere il sequente ∆Γ⇒⇒,!α  come "usando un certo numero 
di volte α  ed usando Γ , otteniamo ∆ " e di leggere il sequente α?,∆Γ⇒⇒  come 
"usando Γ , otteniamo ∆  ed un certo numero di α ". Questo significa che con le regole 
                                                 
5
 Nella letteratura sulla logica lineare per i due connettivi in questione i nomi più in uso sono "storage" 
(immagazzinamento) per "!" e "co-storage" per il suo duale "?" questo rende immediatamente il senso dei 
due connettivi da un punto di vista di sensibilità alle risorse. 
 18 
per ! noi vogliamo poter esprimere che per ogni fissato valore di i (0≥i ) che 
∆Γ
∆Γ
⇒
⇒
,!
,
α
α
i
 dove  volte),...(, i
i
ααα = , cioè la nostra sintassi deve poter dimostrare 
)0(
,!
=
⇒
⇒
i
∆Γ
∆Γ
α
, )1(
,!
,
=
⇒
⇒
i
∆Γ
∆Γ
α
α
, )2(
,!
,,
=
⇒
⇒
i
∆Γ
∆Γ
α
αα
,… (per ogni i). 
Questo scopo è ottenuto con le seguenti regole per il connettivo "!": 
 
! sx
∆⇒Γ
∆⇒Γ
,!
,
α
α
 !-ind. 
∆⇒Γ
∆⇒Γ
,!α
 !-contr. 
∆⇒Γ
∆⇒Γ
,!
,!,!
α
αα
 
Queste tre regole ci permettono di dimostrare facilmente tutt i gli infinit i casi esp ressi 
sopra. 
Simmetricamente con le regole
6
 per "?" 
 
? dx
α
α
?,
,
∆Γ
∆Γ
⇒
⇒
 ?-ind. 
α?,∆⇒Γ
∆⇒Γ
 ?-contr. 
α
αα
?,
?,?,
∆⇒Γ
∆⇒Γ
 
 
Si dimostra che  
)0(
?,
=
⇒
⇒
i
α∆Γ
∆Γ
, )1(
?,
,
=
⇒
⇒
i
α
α
∆Γ
∆Γ
, )2(
?,
,,
=
⇒
⇒
i
α
αα
∆Γ
∆Γ
,… (per ogni i). 
 
I due nuovi connettivi, quindi, non modificano la concezione lineare dei sequenti, ma 
con ∆Γ⇒⇒,!α  ci permettono di esprimere nel sistema formale che "esiste n tale che 
∆Γ⇒⇒,,...,
1 n
αα " e con α?,∆Γ⇒⇒  che "esiste n tale che 
n
αα ,...,,
1
∆Γ⇒⇒ ". 
Questi due connettivi praticamente, in questo modo reintroducono l'indebolimento e la 
contrazione condizionatamente alle formule contrassegnate da essi. 
 
L'uso dei quantificatori da LK a CLL non subisce alterazioni, perciò ne tratteremo 
quando definiremo le regole di inferenza. 
Ora passiamo a definire in maniera più rigorosa il nostro sistema formale.