Girard, J.-Y. Girard. Linear Logic, its syntax and semantics, Advances in Linear Logic, eds, Lafont, Regnier, pp. 1-42. (CUP,LMSLNS_222,1995).pdf

文档介绍：LINEAR LOGIC
ITS SYNT AX AND
SEMANTICS
Jean
Yv es Girard
Lab oratoire de Math
ematiques Discr
etes
UPR
CNRS

Av en ue de Lumin y
Case
F
Marseille Cedex
gir ar d
lmd
univ
mrs
fr
THE SYNT AX OF LINEAR LOGIC
The connectiv es of linear logic
Linear logic is not an alternativ e logic
it should rather b e seen as an exten
sion of usual logic
Since there is no hop e to mo dify the extan t classical or

in tuitionistic connectiv es
linear logic in tro duces new connectiv es
Exp onen tials
actions vs situations
Classical and in tuitionistic logics deal with stable truths
if A and A
B
then B
but A stil l holds
This is p erfect in mathematics
but wrong in real life
since real implication
is c ausal
A causal implication cannot b e iterated since the conditions are
mo di
ed after its use
this pro cess of mo di
cation of the premises
conditions
is kno wn in ph ysics as r e action
F or instance
if A is to sp end
on a pac kof
cigarettes and B is to get them
y ou lose
in this pro cess
and y ou cannot do
it a second time
The reaction here w as that
w en t out of y our p o c k et
The
rst ob jection to that view is that there are in mathematics
in real life
cases
where reaction do es not exist or can b e neglected
think of a lemm awhic his
forev er true
or of a Mr
Soros
who has almost an in
nite amoun t of dollars
Witness the fate of non
monotonic
logics
who tried to tamp er with logical rules with
out c hanging the basic op erations

Jean
Yv es Girard
Suc h cases are situations in the sense of stable truths
Our logical re
nemen ts
should not prev en t us to cop e with situations
and there will b e a sp eci
c kind
of connectiv es
exp onentials
and
whic h shall express the iterabilit y
of an action
i
e
the absence of an y reaction
t ypically
A means to sp end as
man y dollars as one needs
If w e use the sym bol