LINEAR LOGIC : ITS SYNTAX AND

SEMANTICS
Jean-Yves Girard
Laboratoire de Mathematiques Discr`etes
UPR 9016 CNRS
163, Avenue de Luminy, Case 930
F-13288 Marseille Cedex 09
girard@[Link]
1 THE SYNTAX OF LINEAR LOGIC
1.1 The connectives of linear logic
Linear logic is not an alternative logic ; it should rather be seen as an exten-
sion of usual logic. Since there is no hope to modify the extant classical or
intuitionistic connectives
1
, linear logic introduces new connectives.
1.1.1 Exponentials : actions vs situations
Classical and intuitionistic logics deal with stable truths :
if A and A B, then B, but A still holds.
This is perfect in mathematics, but wrong in real life, since real implication
is causal. A causal implication cannot be iterated since the conditions are
modied after its use ; this process of modication of the premises (conditions)
is known in physics as reaction. For instance, if A is to spend $1 on a pack of
cigarettes and B is to get them, you lose $1 in this process, and you cannot do
it a second time. The reaction here was that $1 went out of your pocket. The
rst objection to that view is that there are in mathematics, in real life, cases
where reaction does not exist or can be neglected : think of a lemma which is
forever true, or of a Mr. Soros, who has almost an innite amount of dollars.
1. Witness the fate of non-monotonic logics who tried to tamper with logical rules with-
out changing the basic operations . . .
1
2 Jean-Yves Girard
Such cases are situations in the sense of stable truths. Our logical renements
should not prevent us to cope with situations, and there will be a specic kind
of connectives (exponentials, ! and ? ) which shall express the iterability
of an action, i.e. the absence of any reaction ; typically !A means to spend as
many dollars as one needs. If we use the symbol (linear implication) for
causal implication, a usual intuitionistic implication A B therefore appears
as
A B = (!A) B
i.e. A implies B exactly when B is caused by some iteration of A. This formula
is the essential ingredient of a faithful translation of intuitionistic logic into
linear logic ; of course classical logic is also faithfully translatable into linear
logic
2
, so nothing will be lost . . . It remains to see what is gained.
1.1.2 The two conjunctions
In linear logic, two conjunctions (times) and & (with) coexist. They cor-
respond to two radically dierent uses of the word and. Both conjunctions
express the availability of two actions ; but in the case of , both will be done,
whereas in the case of &, only one of them will be performed (but we shall
decide which one). To understand the distinction consider A,B,C :
A : to spend $1,
B : to get a pack of Camels,
C : to get a pack of Marlboro.
An action of type A will be a way of taking $1 out of ones pocket (there may
be several actions of this type since we own several notes). Similarly, there are
several packs of Camels at the dealers, hence there are several actions of type
B. An action type AB is a way of replacing any specic dollar by a specic
pack of Camels.
Now, given an action of type AB and an action of type AC, there will be
no way of forming an action of type ABC, since for $1 you will never get
what costs $2 (there will be an action of type AA BC, namely getting
two packs for $2). However, there will be an action of type AB&C, namely
the superimposition of both actions. In order to perform this action, we have
rst to choose which among the two possible actions we want to perform, and
then to do the one selected. This is an exact analogue of the computer in-
struction if . . . then . . . else . . . : in this familiar case, the parts then . . .
and else . . . are available, but only one of them will be done. Although &
has obvious disjunctive features, it would be technically wrong to view it as a
disjunction : the formulas A&B A and A&BB are both provable (in the
2. With some problems, see 2.2.7
Linear logic : its syntax and semantics 3
same way
&
, to be introduced below, is technically a disjunction, but has
prominent conjunctive features). There is a very important property, namely
the equivalence
3
between !(A&B) and !A!B.
By the way, there are two disjunctions in linear logic :
(plus) which is the dual of &, expresses the choice of one action
between two possible types ; typically an action of type A B C will be
to get one pack of Marlboro for the dollar, another one is to get the pack of
Camels. In that case, we can no longer decide which brand of cigarettes we
shall get. In terms of computer science, the distinction &/ corresponds to
the distinction outer/inner non determinism.

&
(par) which is the dual of , expresses a dependency between two
types of actions ; the meaning of
&
is not that easy, let us just say
anticipating on the introduction of linear negation that A
&
B can either
be read as A

B or as B

A, i.e.
&
is a symmetric form of ;
in some sense,
&
is the constructive contents of classical disjunction.
1.1.3 Linear negation
The most important linear connective is linear negation ( )

(nil ). Since linear

implication will eventually be rewritten as A

&
B, nil is the only negative
operation of logic. Linear negation behaves like transposition in linear algebra
(A B will be the same as B

), i.e. it expresses a duality, that is a

change of standpoint :
action of type A = reaction of type A

(other aspects of this duality are output/input, or answer/question).

The main property of ( )

is that A

can, without any problem, be identied

with A like in classical logic. But (as we shall see in Section 2) linear logic
has a very simple constructive meaning, whereas the constructive contents
of classical logic (which exists, see 2.2.7) is by no means . . . obvious. The
involutive character of nil ensures De Morgan-like laws for all connectives
and quantiers, e.g.
xA = (xA

which may look surprising at rst sight, especially if we keep in mind that the
existential quantier of linear logic is eective : typically, if one proves xA,
then one proves A[t/x] for a certain term t. This exceptional behaviour of nil
comes from the fact that A

negates (i.e. reacts to) a single action of type A,

whereas usual negation only negates some (unspecied) iteration of A, what
3. This is much more than an equivalence, this is a denotational isomorphism, see 2.2.5
4 Jean-Yves Girard
usually leads to a Herbrand disjunction of unspecied length, whereas the idea
of linear negation is not connected to anything like a Herbrand disjunction.
Linear negation is therefore more primitive, but also stronger (i.e. more dicult
to prove) than usual negation.
1.1.4 States and transitions
A typical consequence of the excessive focusing of logicians on mathematics is
that the notion of state of a system has been overlooked.
We shall consider below the example of states in (summary !) chemistry, con-
sisting of lists of molecules involved in a reaction (but a similar argumentation
can be applied to Petri nets, as rst observed by Asperti [4], a state being
a distribution of tokens or the game of chess a state being the current
position during a play etc.)
Observe that summary chemistry is modelled according to precise protocols,
hence can be formalized : it can eventually be written in mathematics. But
in all cases, one will have to introduce an extraneous temporal parameter,
and the formalization will explain, in classical logic, how to pass from the
state S (modelled as (S, t)) to a new one (modelled as (S

, t +1)). This is very

awkward, and it would be preferable to ignore this ad hoc temporal parameter.
In fact, one would like to represent states by formulas, and transitions by
means of implications of states, in such a way that S

is accessible from S
exactly when S S

is provable from the transitions, taken as axioms. But

here we meet the problem that, with usual logic, the phenomenon of updating
cannot be represented. For instance take the chemical equation
2H
2
+ O
2
2H
2
O.
A paraphrase of it in current language could be
H
2
and H
2
and O
2
imply H
2
O and H
2
O.
Common sense knows how to manipulate this as a logical inference ; but this
common sense knows that the sense of and here is not idempotent (because
the proportions are crucial) and that once the starting state has been used to
produce the nal one, it cannot be reused. The features which are needed here
are those of to represent and and to represent imply ; a correct
representation will therefore be
H
2
H
2
O
2
H
2
OH
2
O
and it turns out that if we take chemical equations written in this way as
axioms, then the notion of linear consequence will correspond to the notion of
Linear logic : its syntax and semantics 5
accessible state from an initial one. In this example we see that it is crucial
that the two following principles of classical logic
A B A (weakening)
A A A (contraction)
become wrong when is replaced by and is replaced by (contraction
would say that the proportions do not matter, whereas weakening would enable
us to add an atom of carbon to the left, that would not be present on the right).
To sum up our discussion about states and transitions : the familiar notion of
theory classical logic + axioms should therefore be replaced by :
theory = linear logic + axioms + current state.
The axioms are there forever ; but the current state is available for a single
use : hence once it has been used to prove another state, then the theory is
updated, i.e. this other state becomes the next current state. The axioms can
of course be replaced by formulas !A.
This remark is the basis for potential applications to AI, see [11], this volume :
in linear logic certain informations can be logically erased, i.e. the process of
revision can be performed by means of logical consequence. What makes it
possible is the distinction between formulas !A that speak of stable facts (like
the rule of a game) and ordinary ones (that speak about the current state).
The impossibility of doing the same thing in classical logic comes from the fact
that this distinction makes no sense classically, so any solution to the updating
of states would ipso facto also be a solution to the updating of the rule of the
game
4
.
These dynamical features have been fully exploited in Linear Logic Program-
ming, as rst observed in [3]. The basic idea is that the resolution method
for linear logic (i.e. proof-search in linear sequent calculus) updates the con-
text, in sharp contrast to intuitionistic proof-search, for which the contexts are
monotonic. Updating, inheritance, parallelism are the main features of linear
logic programming.
1.1.5 The expressive power of linear logic
Due to the presence of exponentials, linear logic is as expressive as classical or
intuitionistic logic. In fact it is more expressive. Here we must be cautious :
4. In particular it would update classical mathematics : can anybody with a mathemat-
ical background imagine a minute that commutative algebra can be updated into non-
commutative algebra ?
6 Jean-Yves Girard
in some sense everything that can be expressed can be expressed in classical
logic . . . so what ? In fact we have the same problem with intuitionistic logic,
which is also more expressive than classical logic.
The basic point is that linear logic connectives can express features that classi-
cal logic could only handle through complex and ad hoc translations. Typically
the update of the position m of a pawn inside a chess game with current board
M into m

(yielding a new current board M

) can be classically handled by

means of an implication involving M and M

(and additional features, like

temporal markers), whereas the linear implication m m

will do exactly
the same job. The introduction of new connectives is therefore the key to a
more manageable way of formalizing ; also the restriction to various fragments
opens the area of languages with specic expressive power, e.g. with a given
computational complexity.
It is in fact surprising how easily various kinds of abstract machines (besides
the pioneering case of Petri nets) can be faithfully translated in linear logic.
This is perhaps the most remarkable feature in the study of the complexity of
various fragments of linear logic initiated in [25]. See [24], this volume. It is
to be remarked that these theorems strongly rely on cut-elimination.
1.1.6 A Far West : non-commutative linear logic
In summary chemistry, all the molecules which contribute to a given state
are simultaneously available ; however one nds other kinds of problems in
which this is not the case. Typically think of a stack a
0
. . . a
n
in which a
n1
is
hidden by a
n
: if we represent such a state by a conjunction then another
classical principle, namely
A B B A (exchange)
fails, which suggests yet a more drastic modication, i.e. non-commutative
linear logic. By the way there is an interesting preguration of linear logic
in the literature, namely Lambeks syntactic calculus, introduced in 1958 to
cope with certain questions of linguistic, see [23], this volume. This system is
based on a non-commutative , which in turn induces two linear implications.
There would be no problems to enrich the system with additives & and ,
but the expressive power remains extremely limited. The missing items are
exponentials and negation :
Exponentials stumble on the question of the equivalence between !(A&B)
and !A!B, which is one of the main highway of linear logic : since & is
commutative, the Times should be commutative in this case . . . or should
Linear logic : its syntax and semantics 7
one have simultaneously a commutative Times, in which case the relation
between both types of conjunctions should be understood.
Linear negation is delicate, since there are several possibilities, e.g. a single
negation, like in cyclic linear logic as expounded in [27] or two negations,
like the two linear implications, in which case the situation may become
extremely intricate. Abrusci, see [2], this volume, proposed an interesting
solution with two negations.
The problem of nding the non-commutative system is delicate, since al-
though many people will agree that non-commutativity makes sense, non-
trivial semantics of non-commutativity are not manyfold. In particular a con-
vincing denotational semantics should be set up. By the way, it has been
observed from the beginning that non-commutative proof-nets should be pla-
nar, which suggests either a planarity restriction or the introduction of braids.
Besides the introduction of a natural semantics, the methodology for acknowl-
edging a non-commutative system would also include the gain of expressive
power w.r.t. the commutative case.
1.2 Linear sequent calculus
1.2.1 Structural rules
In 1934 Gentzen introduced sequent calculus, which is a basic synthetic tool
for studying the laws of logic. This calculus is not always convenient to build
proofs, but it is essential to study their properties. (In the same way, Hamil-
tons equations in mechanics are not very useful to solve practical problems
of motion, but they play an essential role when we want to discuss the very
principles of mechanics.) Technically speaking, Gentzen introduced sequents,
i.e. expressions where (= A
1
, . . . , A
n
) and (= B
1
, . . . , B
m
) are nite
sequences of formulas. The intended meaning of is that
A
1
and . . . and A
n
imply B
1
or . . . or B
m
but the sense of and, imply, or has to be claried. The calculus is di-
vided into three groups of rules (identity, structural, logical), among which the
structural block has been systematically overlooked. In fact, a close inspection
shows that the actual meaning of the words and, imply, or, is wholly in
the structural group and it is not too excessive to say that a logic is essentially
a set of structural rules ! The structural rules considered by Gentzen (respec-
tively weakening, contraction, exchange)
8 Jean-Yves Girard

A,

, A
A, A,
A,
, A, A
, A

() ()
are the sequent calculus formulation of the three classical principles already
met and criticized. Let us detail them.
Weakening. Weakening opens the door for fake dependencies : from a
sequent we can get another one

by extending the sequences ,

. Typically, it speaks of causes without eect, e.g. spending $1 to get noth-
ing not even smoke ; but it is an essential tool in mathematics (from B
deduce A B) since it allows us not to use all the hypotheses in a deduction.
It will rightly be rejected from linear logic.
Anticipating on linear sequent calculus, we see that the rule says that is
stronger than & :
A A
A, B A
B B
A, B B
A, B A&B
A B A&B
Ane linear logic is the system of linear logic enriched (?) with weakening.
There is no much use for this system since the ane implication between A
and B can be faithfully mimicked by 1&A B. Although the system enjoys
cut-elimination, it has no obvious denotational semantics, like classical logic.
Contraction. Contraction is the ngernail of innity in propositional cal-
culus : it says that what you have, will always keep, no matter how you use
it. The rule corresponds to the replacement of by

where

and

come from and by identifying several occurrences of the same

formula (on the same side of ). To convince oneself that the rule is about
innity (and in fact that without it there is no innite at all in logic), take the
formula I : xy x < y (together with others saying that < is a strict order).
This axiom has only innite models, and we show this by exhibiting 1, 2, 3,
4, . . . distinct elements ; but, if we want to exhibit 27 distinct elements, we
Linear logic : its syntax and semantics 9
are actually using I 26 times, and without a principle saying that 26 I can be
contracted into one, we would never make it ! In other terms innity does not
mean many, but always. Another innitary feature of the rule is that it is the
only responsible for undecidability
5
: Gentzens subformula property yields a
decision method for predicate calculus, provided we can bound the length of
the sequents involved in a cut-free proof, and this is obviously the case in the
absence of contraction.
In linear logic, both contraction and weakening will be forbidden as structural
rules. But linear logic is not logic without weakening and contraction, since it
would be nonsense not to recover them in some way : we have introduced a
new interpretation for the basic notions of logic (actions), but we do not want
to abolish the old one (situations), and this is why special connectives (expo-
nentials ! and ? ) will be introduced, with the two missing structurals as
their main rules. The main dierence is that we now control in many cases
the use of contraction, which one should not forget it means controlling
the length of Herbrand disjunctions, of proof-search, normalization procedures,
etc.
Whereas the meaning of weakening is the fact that is stronger than &,
contraction means the reverse implication : using contraction we get :
A A
A&B A
B B
A&B B
A&B, A&B A B
A&B A B
It is dicult to nd any evidence of such an implication outside classical logic.
The problem is that if we accept contraction without accepting weakening too,
we arrive at a very confusing system, which would correspond to an imperfect
analysis of causality : consider a petrol engine, in which petrol causes the mo-
tion (P M) ; weakening would enable us to call any engine a petrol engine
(from M deduce P M), which is only dishonest, but contraction would
be miraculous : from P M we could deduce P P M, i.e. that the petrol
is not consumed in the causality. This is why the attempts of philosophers to
build various relevance logics out of the only rejection of weakening were never
very convincing
6
5. If we stay rst-order : second-order linear logic is undecidable in the absence of expo-
nentials, as recently shown by Lafont (unpublished), see also [24].
6. These systems are now called substructural logics, which is an abuse, since most of the
calculi associated have no cut-elimination . . . .
10 Jean-Yves Girard
Intuitionistic logic accepts contraction (and weakening as well), but only on the
left of sequents : this is done in (what can now be seen as) a very hypocritical
way, by restricting the sequents to the case where consists of one formula,
so that we are never actually in position to apply a right structural rule. So,
when we have a cut-free proof of A, the last rule must be logical, and this has
immediate consequences, e.g. if A is y B then B[t] has been proved for some
t, etc. These features, that just come from the absence of right contraction,
will therefore be present in linear logic, in spite of the presence of an involutive
negation.
Exchange. Exchange expresses the commutativity of multiplicatives : we
can replace with

where

and

are obtained from and

by permutations of their formulas.
1.2.2 Linear sequent calculus
In order to present the calculus, we shall adopt the following notational sim-
plication : formulas are written from literals p, q, r, p

, q

, r

, etc., and
constants 1, , , 0 by means of the connectives ,
&
, &, (binary), !,
? (unary), and the quantiers x, x. Negation is dened by De Morgan
equations, and linear implication is also a dened connective :
1

:=

:= 0
(p)

:= p

(A B)

:= A

&
B

(A&B)

:= A

(!A)

:= ?A

(x A)

:= x A

:= 1
0

:=
(p

:= p
(A
&
B)

:= A

(A B)

:= A

&B

(?A)

:= !A

(x A)

:= x A

A B := A

&
B
The connectives ,
&
, , together with the neutral elements 1 (w.r.t. )
and (w.r.t.
&
) are called multiplicatives ; the connectives &and , together
with the neutral elements (w.r.t. &) and 0 (w.r.t ) are called additives ;
the connectives ! and ? are called exponentials. The notation has been cho-
sen for its mnemonic virtues : we can remember from the notation that is
multiplicative and conjunctive, with neutral 1, is additive and disjunctive,
with neutral 0, that
&
is disjunctive with neutral , and that &is conjunctive
with neutral ; the distributivity of over is also suggested by our notation.
Sequents are right-sided, i.e. of the form ; general sequents can
be mimicked as

, .
Linear logic : its syntax and semantics 11
Identity / Negation
(identity)
A, A

, A A

,
(cut)
,
Structure

(exchange :

is a permutation of )

Logic
(one)
1

(false)
,
, A B,
(times)
, A B,
, A, B
(par)
, A
&
B
(true)
,
(no rule for zero)
, A , B
(with)
, A&B
, A
(left plus)
, A B
, B
(right plus)
, A B
?, A
(of course)
?, !A

(weakening)
, ?A
, A
(dereliction)
, ?A
, ?A, ?A
(contraction)
, ?A
, A
(for all : x is not
free in )
, x A
, A[t/x]
(there is)
, x A
1.2.3 Comments
The rule for
&
shows that the comma behaves like a hypocritical
&
(on
the left it would behave like ) ; and, or, imply are therefore read as
,
&
, .
In a two-sided version the identity rules would be
12 Jean-Yves Girard
A A
, A A,
, ,
and we therefore see that the ultimate meaning of the identity group (and the
only principle of logic beyond criticism) is that A is A ; in fact the two rules
say that A on the left (represented by A

in the right-sided formulation) is

stronger (resp. weaker) than A on the right. The meaning of the identity group
is to some extent blurred by our right-sided formulation, since the group may
also be seen as the negation group.
The logical group must be carefully examined :
multiplicatives and additives : notice the dierence between the rule for
and the rule for & : requires disjoint contexts (which will never be
identied unless ? is heavily used) whereas & works with twice the same
context. If we see the contexts of A as the price to pay to get A, we recover
our informal distinction between the two conjunctions. In a similar way, the
two disjunctions are very dierent, since requires one among the premises,
whereas
&
requires both).
exponentials : ! and ? are modalities : this means that !A is simultaneously
dened on all formulas : the of course rule mentions a context with ?, which
means that ? (or !

) is known. !A indicates the possibility of using A ad

libitum ; it only indicates a potentiality, in the same way that a piece of paper
on the slot of a copying machine can be copied . . . but nobody would identify
a copying machine with all the copies it produces ! The rules for the dual
(why not) are precisely the three basic ways of actualizing this potentiality :
erasing (weakening), making a single copy (dereliction), duplicate . . . the
machine (contraction). It is no wonder that the rst relation of linear logic
to computer science was the relation to memory pointed out by Yves Lafont
in [21].
quantiers : they are not very dierent from what they are in usual logic,
if we except the disturbing fact that x is now the exact dual of x. It is
important to remark that x is very close to & (and that x is very close to
).
1.3 Proof-nets
1.3.1 The determinism of computation
For classical and intuitionistic logics, we have an essential property, which
dates back to Gentzen (1934), known as the Hauptsatz, or cut-elimination
theorem ; the Hauptsatz presumably traces the borderline between logic and
Linear logic : its syntax and semantics 13
the wider notion of formal system. It goes without saying that linear logic
enjoys cut-elimination
7
.
Theorem 1
There is an algorithm transforming any proof of a sequent in linear
logic into a cut-free proof of the same sequent.
Proof. The proof basically follows the usual argument of Gentzen ; but
due to our very cautious treatment of structural rules, the proof is in fact much
simpler. There is no wonder, since linear logic comes from a proof-theoretical
analysis of usual logic ! 2
We have now to keep in mind that the Hauptsatz under various disguises,
e.g. normalization in -calculus is used as possible theoretical foundation
for computation. For instance consider a text editor : it can be seen as a set
of general lemmas (the various subroutines about bracketing, the size of pages
etc.), that we can apply to a concrete input, let us say a given page that I write
from the keyboard ; observe that the number of such inputs is practically in-
nite and that therefore our lemmas are about the innite. Now when I feed the
program with a concrete input, there is no longer any reference to innity . . .
In mathematics, we could content ourselves with something implicit like your
input is correct, whereas we would be mad at a machine which answers I can
do it to a request. Therefore, the machine does not only check the correctness
of the input, it also demonstrates it by exhibiting the nal result, which no
longer mentions abstractions about the quasi-innite potentiality of all possible
pages. Concretely this elimination of innity is done by systematically making
all concrete replacements in other terms by running the program. But this
is exactly what the algorithm of cut-elimination does.
This is why the structure of the cut-elimination procedure is essential. And
this structure is quite problematic, since we get problems of permutation of
rules.
Let us give an example : when we meet a conguration
, A
(r)

, A
A

,
(s)
A

(cut)

there is no natural way to eliminate this cut, since the unspecied rules (r)
and (s) do not act on A or A

; then the idea is to forward the cut upwards :

7. A sequent calculus without cut-elimination is like a car without engine
14 Jean-Yves Girard
, A A

,
(cut)
,
(r)

,
(s)

But, in doing so, we have decided that rule (r) should now be rewritten before
rule (s), whereas the other choice
, A A

,
(cut)
,
(s)
,

(r)

would have been legitimate too. The bifurcation starting at this point is usually
irreversible : unless (r) or (s) is later erased, there is no way to interchange
them. Moreover the problem stated was completely symmetrical w.r.t. left and
right, and we can of course arbitrate between the two possibilities by many
bureaucratical tricks ; we can decide that left is more important than right,
but this choice will at some moment conict with negation (or implication)
whose behaviour is precisely to mimic left by right . . . Lets be clear : the
taxonomical devices that force us to write (r) before (s) or (s) before (r) are
not more respectable than the alphabetical order in a dictionary. One should
try to get rid of them, or at least, ensure that their eect is limited. In fact
denotational semantics, see chapter 2 is very important in this respect, since
the two solutions proposed have the same denotation. In some sense the two
answers although irreversibly dierent are consistent. This means that if
we eliminate cuts in a proof of an intuitionistic disjunction A B (or a
linear disjunction AB) and eventually get a proof of A or a proof of B,
the side (A or B) is not aected by this bifurcation. However, we would like to
get better, namely to have a syntax in which such bifurcations do not occur.
In intuitionistic logic (at least for the fragment , , ) this can be obtained
by replacing sequent calculus by natural deduction. Typically the two proofs
just written will get the same associated deduction . . . In other terms natural
deduction enjoys a conuence (or Church-Rosser) property : if

then
there is

such that

, i.e. bifurcations are not irreversible.

1.3.2 Limitations of natural deduction
Let us assume that we want to use natural deduction to deal with proofs in
linear logic ; then we run into problems.
Linear logic : its syntax and semantics 15
(1) Natural deduction is not equipped to deal with classical symmetry : sev-
eral hypotheses and one (distinguished) conclusion. To cope with symmetrical
systems one should be able to accept several conclusions at once . . . But then
one immediately loses the tree-like structure of natural deductions, with its ob-
vious advantage : a well-determined last rule. Hence natural deduction cannot
answer the question. However it is still a serious candidate for an intuitionistic
version of linear logic ; we shall below only discuss the fragment (, ), for
which there is an obvious natural deduction system :
[A]

B
(-intro)
A B
A A B
(-elim)
B
A B
(-intro)
A B
A B
[A][B]

C
(-elim)
C
As usual a formula between brackets indicates a discharge of hypothesis ; but
here the discharge should be linear, i.e. exactly one occurrence is discharged
(discharging zero occurrence is weakening, discharging two occurrences is con-
traction). Although this system succeeds in identifying a terric number of
interversion-related proofs, it is not free from serious defects, more precisely :
(2) In the elimination rules the formula which bears the symbol ( or )
is written as a hypothesis ; this is user-friendly, but goes against the actual
mathematical structure. Technically this premise is in fact the actual conclu-
sion of the rule (think of main hypotheses or headvariables), which is therefore
written upside down. However this criticism is very inessential.
(3) Due to discharge, the introduction rule for (and the elimination rule
for ) does not apply to a formula, but to a whole proof. This global character
of the rule is quite a serious defect.
(4) Last but not least, the elimination rule for mentions an extraneous
formula C which has nothing to do with A B. In intuitionistic natural
deduction, we have the same problem with the rules for disjunction and exis-
tence which mention an extraneous formula C ; the theory of normalization
16 Jean-Yves Girard
(commutative conversions) then becomes extremely complex and awkward.
1.3.3 The identity links
We shall nd a way of xing defects (1)(4) in the context of the multiplicative
fragment of linear logic, i.e. the only connectives and
&
(and also implicitly
). The idea is to put everything in conclusion ; however, when we pass
from a hypothesis to a conclusion we must indicate the change by means of
a negation symbol. There will be two basic links enabling one to replace a
hypothesis with a conclusion and vice versa, namely
(axiom link)
A A

(cut link)
A A

By far the best explanation of these two links can be taken from electronics.
Think of a sequent as the interface of some electronic equipment, this inter-
face being made of plugs of various forms A
1
, . . . , A
n
; the negation corresponds
to the complementarity between male and female plugs. Now a proof of can
be seen as any equipment with interface . For instance the axiom link is such
a unit and it exists in everyday life as the extension cord :
A

A
Now, the cut link is well explained as a plugging :
. . .

. . .
A A

The main property of the extension cord is that

. . .

behaves like
. . .

It seems that the ultimate, deep meaning of cut-elimination is located there.

Moreover observe that common sense would forbid self-plugging of an extension
cord :
Linear logic : its syntax and semantics 17
which would correspond, in terms of proof-nets to the incestuous conguration :
A A

which is not acknowledged as a proof-net ; in fact in some sense the ultimate

meaning of the correctness criterion that will be stated below is to forbid such
a conguration (and also disconnected ones).
1.3.4 Proof-structures
If we accept the additional links :
A B
(times link)
A B
A B
(par link)
A
&
B
then we can associate to any proof of in linear sequent calculus a graph-
like proof-structure with as conclusions the formulas of . More precisely :
1. To the identity axiom associate an axiom link.
2. Do not interpret the exchange rule (this rule does not aect conclusions ;
however, if we insist on writing a proof-structure on a plane, the eect of the
rule can be seen as introducing crossings between axiom links ; planar proof-
structures will therefore correspond to proofs in some non-commutative vari-
ants of linear logic).
3. If a proof-structure ending with , A and B has been associated to a
proof of , A, B and if one now applies a par rule to this proof to
get a proof

of , A
&
B , then the structure

associated to

will be
obtained from by linking A and B via a par link : therefore A and B are
no longer conclusions, and a new conclusion A
&
B is created.
4. If
1
is a proof of , A and
2
is a proof of B, to which proof-
structures
1
and
2
have been associated, then the proof

obtained from
1
and
2
by means of a times rule is interpreted by means of the proof structure
obtained from
1
and
2
by linking A and B together via a times link.
Therefore A and B are no longer conclusions and a new conclusion A B
is created.
5. If
1
is a proof of , A and
2
is a proof of A

, to which
proof-structures
1
and
2
have been associated, then the proof

obtained
from
1
and
2
by means of a cut rule is interpreted by means of the proof
structure obtained from
1
and
2
by linking A and A

together via a cut

link. Therefore A and A

are no longer conclusions.

18 Jean-Yves Girard
An interesting exercise is to look back at the natural deduction of linear logic
and to see how the four rules can be mimicked by proof-structures :
A

&
B
A

A
.
.
.
B
A

&
B A B

A B

B
A B
A B
A B A

&
B

C
A B
.
.
. .
.
.
This shows that once everything has been put in conclusion
-intro = -elim = par link ;
-elim = -intro = times link.
1.3.5 Proof-nets
A proof-structure is nothing but a graph whose vertices are (occurrences of)
formulas and whose edges are links ; moreover each formula is the conclusion of
exactly one link and the premise of at most one link. The formulas which are
not premises are the conclusions of the structure. Inside proof-structures, let
us call proof-nets those which can be obtained as the interpretation of sequent
calculus proofs. Of course most structures are not nets : typically the de-
nition of a proof-structure does not distinguish between -links and
&
-links
whereas conjunction is surely dierent from disjunction.
The question which now arises is to nd an independent characterization of
proof-nets. Let us explain why this is essential :
1. If we dene proof-nets from sequent calculus, this means that we work with
a proof-structure together with a sequentialization, in other terms a step by
step construction of this net. But this sequentialization is far from being
unique, typically there might be several candidates for the last rule of a
given proof-net. In practice, we may have a proof-net with a given sequen-
tialization but we may need to use another one : this means that we will
spend all of our energy on problems of commutation of rules, as with old
Linear logic : its syntax and semantics 19
sequent calculus, and we will not benet too much from the new approach.
Typically, if a proof-net ends with a splitting -link, (i.e. a link whose re-
moval induces two disconnected structures), we would like to conclude that
the last rule can be chosen as -rule ; working with a sequentialization this
can be proved, but the proof is long and boring, whereas, with a criterion,
the result is immediate, since the two components inherit the criterion.
2. The distinction between and and or has always been explained in se-
mantical terms which ultimately use and and or ; a purely geometrical
characterization would therefore establish the distinction on more intrinsic
grounds.
The survey of Yves Lafont [22] (this volume) contains the correctness crite-
rion (rst proved in [12] and simplied by Danos and Regnier in [9]) and the
sequentialization theorem. From the proof of the theorem, one can extract
a quadratic algorithm checking whether or not a given multiplicative proof-
structure is a proof-net. Among the uses of multiplicative proof-nets, let us
mention the questions of coherence in monoidal closed categories [6].
1.3.6 Cut-elimination for proof-nets
The crucial test for the new syntax is the possibility to handle syntactical
manipulations directly at the level of proof-nets (therefore completely ignoring
sequent calculus). When we meet a cut link
A A

we look at links whose conclusions are A and A

:
(1) One of these links is an axiom link, typically :
A
.
.
.
.
.
.
A

such a conguration can be replaced by

.
.
.
A

.
.
.
however the graphism is misleading, since it cannot be excluded that the two
occurrences of A

in the original net are the same ! But this would correspond
to a conguration
A A

in , and such congurations are excluded by the correctness criterion.

20 Jean-Yves Girard
(2) If both formulas are conclusions of logical links for and
&
, typically
B C
B C B

&
C

.
.
.
.
.
.
.
.
.
.
.
.
then we can replace it by
B C
.
.
.
.
.
.
.
.
.
B

.
.
.
and it is easily checked that the new structure still enjoys the correctness
criterion. This cut-elimination procedure has very nice features :
1. It enjoys a Church-Rosser property (immediate).
2. It is linear in time : simply observe that the proof-net shrinks with any appli-
cation of steps (1) and (2) ; this linearity is the start of a line of applications
to computational complexity.
3. The treatment of the multiplicative fragment is purely local ; in fact all
cut-links can be simultaneously eliminated. This must have something to
do with parallelism and recently Yves Lafont developed his interaction nets
as a kind of parallel machine working like proof-nets [22], this volume.
1.3.7 Extension to full linear logic
Proof-nets can be extended to full linear logic. In the case of quantiers one
uses unary links :
A[y/x]
xA
A[t/x]
xA
in the x-link an eigenvariable y must be chosen ; each x-link must use a dis-
tinct eigenvariable (as the name suggests). The sequentialization theorem can
be extended to quantiers, with an appropriate extension of the correctness
criterion.
Additives and neutral elements also get their own notion of proof-nets [17], as
well as the part of the exponential rules which does not deal with !. Although
this extension induces a tremendous simplication of the familiar sequent cal-
culus, it is not as satisfactory as the multiplicative/quantier case.
Linear logic : its syntax and semantics 21
Eventually, the only rule which resists to the proof-net technology is the !-
rule. For such a rule, one must use a box, see [22]. The box structure has
a deep meaning, since the nesting of boxes is ultimately responsible for cut-
elimination.
1.4 Is there a unique logic ?
1.4.1 LU
By the turn of the century the situation concerning logic was quite simple :
there was basically one logic (classical logic) which could be used (by changing
the set of proper axioms) in various situations. Logic was about pure reason-
ing. Brouwers criticism destroyed this dream of unity : classical logic was not
adapted to constructive features and therefore lost its universality. By the end
of the century we are now faced with an incredible number of logics some
of them only named logics by antiphrasis, some of them introduced on se-
rious grounds . Is still logic about pure reasoning? In other terms, could
there be a way to reunify logical systems let us say those systems with a
good sequent calculus into a single sequent calculus. Could we handle the
(legitimate) distinction classical/intuitionistic not through a change of system,
but through a change of formulas? Is it possible to obtain classical eects by
restricting one to classical formulas? etc.
Of course there are surely ways to achieve this by cheating, typically by con-
sidering a disjoint union of systems . . . All these jokes will be made impossible
if we insist on the fact that the various systems represented should freely com-
municate (and for instance a classical theorem could have an intuitionistic
corollary and vice versa).
In the unied calculus LU see [14], classical, linear, and intuitionistic logics
appear as fragments. This means that one can dene notions of classical, in-
tuitionistic, or linear sequents and prove that a cut-free proof of a sequent in
one of these fragments is wholly inside the fragment ; of course a proof with
cuts has the right to use arbitrary sequents, i.e. the fragments can freely com-
municate.
Perhaps the most interesting feature of this new system is that the classical,
intuitionistic and linear fragments of LU are better behaved than the original
sequent calculi. In LU the distinction between several styles of maintenance
(e.g. rule of the game vs current state) is particularly satisfactory. But
after all, LUis little more than a clever reformulation of linear sequent calculus.
22 Jean-Yves Girard
1.4.2 LLL and ELL
This dream of unity stumbles on a new fact : the recent discovery [16] of
two systems which denitely diverge from classical or intuitionistic logic, LLL
(light linear logic) and ELL (elementary linear logic). They come from the
basic remark that, in the absence of exponentials, cut-elimination can be per-
formed in linear time. This result (which is conspicuous from a proof-net
argument
8
), holds for lazy cut-elimination, which does not normalize above
&-rules, and which is enough for algorithmic purposes ; notice that the result
holds without regards for the kind of quantiers rst or second order
used. However the absence of exponentials renders such systems desperately
inexpressive. The rst attempt to expand this inexpressive system while keep-
ing interesting complexity bounds was not satisfactory : BLL (bounded linear
logic) [19] had to keep track of polynomial I/O bounds that induced polytime
complexity eects, but the price paid was obviously too much.
The problem to solve was therefore to nd restriction(s) on the exponentials
which ensure :
cut-elimination, (hence consistency) for naive set-theory, i.e. full compre-
hension
the familiar equivalence between !(A&B) and !A!B
Two systems have been found, both based on the idea that normalization
should respect the depth of formulas (with respect to the nesting of !-boxes).
Normalization is performed in linear time at depth 0, and induces some dupli-
cation of bigger depths, then it is performed at depth 1, etc. and eventually
stops, since the total depth does not change. The global complexity there-
fore depends on the (xed) global depth and on the number of duplications
operated by the cleansing of a given level.
In LLL the sizes of inner boxes are multiplied by a factor corresponding
to the outer size. The global procedure is therefore done in a time which
is a polynomial in the size (with a degree depending of the total depth).
Conversely every polytime algorithm can be represented in LLL.
In ELL the factor is expoenential in the outer size, yielding an elemnetary
complexity for the global procedure, and conversely every elementary algo-
rithm can be represented in ELL. ELL diers from LLL only in the extra
principle !A!B!(A B).
LLL may have interesting applications in complexity theory ; ELL is expres-
sive enough to accommodate a lot of current mathematics.
8. Remember that the size of a proof-net shrinks during cut-elimination
Linear logic : its syntax and semantics 23
2 THE SEMANTICS OF LINEAR LOGIC
2.1 The phase semantics of linear logic
The most traditional, and also the less interesting semantics of linear logic
associates values to formulas, in the spirit of classical model theory. Therefore
it only modelizes provability, and not proofs.
2.1.1 Phase spaces
A phase space is a pair (M, ), where M is a commutative monoid (usually
written multiplicatively) and is a subset of M. Given two subsets X and Y
of M, one can dene X Y := m M ; n X mn Y . In particular,
we can dene for each subset X of M its orthogonal X

:= X . A fact
is any subset of M equal to its biorthogonal, or equivalently any subset of the
form Y

. It is immediate that X Y is a fact as soon as Y is a fact.

2.1.2 Interpretation of the connectives
The basic idea is to interpret all the operations of linear logic by operations
on facts : once this is done the interpretation of the language is more or less
immediate. We shall use the same notation for the interpretation, hence for
instance X Y will be the fact interpreting the tensorization of two formulas
respectively interpreted by X and Y . This suggests that we already know how
to interpret , linear implication and linear negation.
1. times : X Y := mn ; m X n Y

2. par : X
&
Y := (X

3. 1 : 1 := 1

, where 1 is the neutral element of M

4. plus : X Y := (X Y )

5. with : X&Y := X Y
6. zero : 0 :=

7. true : := M
8. of course : !X := (XI)

, where I is the set of idempotents of M which

belong to 1
9. why not : ?X := (X

I)

(The interpretation of exponentials is an improvement of the original denition

of [12] which was awfully ad hoc). This is enough to dene what is a model of
24 Jean-Yves Girard
propositional linear logic. This can easily be extended to yield an interpreta-
tion of quantiers (intersection and biorthogonal of the union). Observe that
the denitions satisfy the obvious De Morgan laws relating and
&
etc. A
non-trivial exercise is to prove the associativity of .
2.1.3 Soundness and completeness
It is easily seen that the semantics is sound and complete :
Theorem 2
A formula A of linear logic is provable i for any interpretation (involving
a phase space (M, )), the interpretation A

of A contains the neutral

element 1.
Proof. Soundness is proved by a straightforward induction. Completeness
involves the building of a specic phase space. In fact we can take as M the
monoid of contexts (i.e. multisets of formulas
9
), whose neutral element is the
empty context, and we dene := ; provable. If we consider the
sets A

:= ; , A provable, then these sets are easily shown to be

facts. More precisely, one can prove (using the identity group) that A

= A

.
It is then quite easy to prove that in fact A

is the value of A in a given model :

this amounts to prove commutations of the style (A B)

= A

(these
proofs are simplied by the fact that in any De Morgan pair one commutation
implies the other, hence we can choose the friendlier commutation). Therefore,
if 1 A

, it follows that A is provable. 2

As far as I know there is no applications for completeness, due to the fact
that there is no known concrete phase spaces to which one could restrict and
still have completeness. Soundness is slightly more fruitful : for instance Yves
Lafont (unpublished, 1994) proved the undecidability of second order propo-
sitional linear logic without exponentials by means of a soundness argument.
This exploits the fact that a phase semantics is not dened as any algebraic
structure enjoying the laws of linear logic, but that it is fully determined from
the choice of a commutative monoid and the interpretation , as soon as the
atoms are interpreted by facts.
2.2 The denotational semantics of linear logic
2.2.1 Implicit versus explicit
First observe that the cut rule is a way to formulate modus ponens. It is the
essential ingredient of any proof. If I want to prove B, I usually try to prove
a useful lemma A and, assuming A, I then prove B. All proofs in nature,
9. We ignore the multiplicity of formulas ?, so that I is the set of contexts ?
Linear logic : its syntax and semantics 25
including the most simple ones, are done in this way. Therefore, there is an
absolute evidence that the cut rule is the only rule of logic that cannot be
removed : without cut it is no longer possible to reason.
Now against common sense Gentzen proved his Hauptsatz ; for classical and
intuitionistic logics (and remember that can be extended to linear logic with-
out problems). This result implies that we can make proofs without cut, i.e.
without lemmas (i.e. without modularity, without ideas, etc.). For instance if
we take an intuitionistic disjunction A B (or a linear plus A B) then a
cut-free proof of it must contain a proof of A or a proof of B. We see at once
that this is articial : who in real life would state A B when he has proved
A? If we want to give a decent status to proof-theory, we have to explain this
contradiction.
Formal reasoning (any reasoning) is about implicit data. This is because it is
more convenient to forget. So, when we prove A B, we never know which
side holds. However, there is inside the sequent calculus formulation a
completely articial use of the rules, i.e. to prove without the help of cut ;
this articial subsystem is completely explicit. The result of Gentzen is a way
to replace a proof by another without cut, which makes explicit the contents
of the original proof. Variants of the Gentzen procedure (normalization in
natural deduction or in -calculus) should also be analysed in that way.
2.2.2 Generalities about denotational semantics
The purpose of denotational semantics is precisely to analyse this implicit con-
tents of proofs. The name comes from the old Fregean opposition sense/denotation :
the denotation is what is implicit in the sense.
The kind of semantics we are interested in is concrete, i.e. to each proof we
associate a set

. This map can be seen as a way to dene an equivalence

between proofs (

) of the same formulas (or sequents), which

should enjoy the following :
1. if normalizes to

, then

;
2. is non-degenerated, i.e. one can nd a formula with at least two non-
equivalent proofs ;
3. is a congruence : this means that if and

have been obtained from

and

by applying the same logical rule, and if

, then

;
4. certain canonical isomorphisms are satised ; among those which are crucial
let us mention :
26 Jean-Yves Girard
involutivity of negation (hence De Morgan),
associativity of par (hence of times).
Let us comment these points :
(1) says that is about cut-elimination.
(2) : of course if all proofs of the same formula are declared to be equivalent,
the contents of is empty.
(3) is the analogue of a Church-Rosser property, and is the key to a modular
approach to normalization.
(4) : another key to modularity is commutation, which means that certain
sequences of operations on proofs are equivalent w.r.t. . It is clear that
the more commutation we get the better, and that we cannot ask too much
a priori. However, the two commutations mentioned are a strict minimum
without which we would get a mess :
involutivity of negation means that we have not to bother about double
negations ; in fact this is the semantical justication of our choice of a
dened negation.
associativity of par means that the bracketing of a ternary par is
inessential ; furthermore, associativity renders possible the identication
of A (B C) with (A B) C.
The denotational semantics we shall present is a simplication of Scott domains
which has been obtained by exploiting the notion of stability due to Berry
(see [18] for a discussion). These drastically simplied Scott domains are called
coherent spaces ; these spaces were rst intended as denotational semantics for
intuitionistic logic, but it turned out that there were a lot of other operations
hanging around. Linear logic rst appeared as a kind of linear algebra built
on coherent spaces ; then linear sequent calculus was extracted out of the
semantics. Recently Ehrhard, see [10], this volume, rened coherent semantics
into hypercoherences, with applications to the question of sequentiality.
2.2.3 Coherent spaces
Denition 1
A coherent space is a reexive undirected graph. In other terms it consists
of a set [X[ of atoms together with a compatibility or coherence relation
between atoms, noted x

y or x

y [mod X] if there is any ambiguity

as to X.
Linear logic : its syntax and semantics 27
A clique a in X (notation a X) is a subset a of X made of pairwise
coherent atoms : a X i x y (x a y a x

y). In fact a
coherent space can be also presented as a set of cliques ; when we want
to emphasize the underlying graph ([X[,

) we call it the web of X.

Besides coherence we can also introduce
strict coherence : x y i x

y and x ,= y,
incoherence : x

y i

(x y),
strict incoherence : x y i

(x

y).
Any of these four relations can serve as a denition of coherent space. Observe
fact that

is the negation of and not of

; this due to the reexivity of

the web.
Denition 2
Given a coherent space X, its linear negation X

is dened by
[X

[ = [X[,
x

y [mod X

] i x

y [mod X].
In other terms, linear negation is nothing but the exchange of coherence and
incoherence. It is obvious that linear negation is involutive :
X

= X.
Denition 3
Given two coherent spaces X and Y , the multiplicative connectives ,
&
, dene a new coherent space Z with [Z[ = [X[ [Y [ ; coherence is
dened by
(x, y)

(x

, y

) [mod X Y ] i
x

[mod X] and y

[mod Y ],
(x, y) (x

, y

) [mod X
&
Y ] i
x x

[mod X] or y y

[mod Y ],
(x, y) (x

, y

) [mod X Y ] i
x

[mod X] implies y y

[mod Y ].
Observe that is dened in terms of

but
&
and in terms of . A lot
of useful isomorphisms can be obtained
1. De Morgan equalities : (X Y )

= X

&
Y

; (X
&
Y )

= X

;
X Y = X

&
Y ;
28 Jean-Yves Girard
2. commutativity isomorphisms : X Y Y X ; X
&
Y Y
&
X ;
X Y Y

;
3. associativity isomorphisms : X(Y Z) (XY ) Z ; X
&
(Y
&
Z)
(X
&
Y )
&
Z ; X(Y Z) (XY )Z ; X(Y
&
Z) (XY )
&
Z.
Denition 4
Up to isomorphism there is a unique coherent space whose web consists
of one atom 0, this space is self dual, i.e. equal to its linear negation.
However the algebraic isomorphism between this space and its dual is
logically meaningless, and we shall, depending on the context, use the
notation 1 or the notation for this space, with the convention that
1

= ,

= 1.
This space is neutral w.r.t. multiplicatives, namely X 1 X, X
&
X,
1 X X, X X

.
This notational distinction is mere preciosity ; one of the main drawbacks
of denotational semantics is that it interprets logically irrelevant properties
. . . but nobody is perfect.
Denition 5
Given two coherent spaces X and Y the additive connectives & and ,
dene a new coherent space Z with [Z[ = [X[ +[Y [ (= [X[ 0 [Y [
1) ; coherence is dened by
(x, 0)

(x

, 0) [mod Z] i x

[mod X],
(y, 1)

(y

, 1) [mod Z] i y

[mod Y ],
(x, 0) (y, 1) [mod X&Y ],
(x, 0) (y, 1) [mod X Y ].
A lot of useful isomorphisms are immediately obtained :
De Morgan equalities : (X&Y )

= X

; (X Y )

= X

&Y

;
commutativity isomorphisms : X&Y Y &X ; X Y Y X ;
associativity isomorphisms : X&(Y &Z) (X&Y )&Z ; X (Y Z)
(X Y ) Z ;
distributivity isomorphisms : X (Y Z) (X Y ) (X Z) ; X
&
(Y &Z) (X
&
Y )&(X
&
Z) ; X (Y &Z) (X Y )&(X Z) ;
(X Y ) Z (X Z)&(Y Z).
The other distributivities fail ; for instance X (Y &Z) is not isomorphic to
(X Y )&(X Z).
Linear logic : its syntax and semantics 29
Denition 6
There is a unique coherent space with an empty web. Although this space
is also self dual, we shall use distinct notations for it and its negation :
and 0.
These spaces are neutral w.r.t. additives : X 0 X, X& X, and
absorbing w.r.t. multiplicatives X 0 0, X
&
, 0 X ,
X .
2.2.4 Interpretation of MALL
MALL is the fragment of linear logic without the exponentials ! and ? .
In fact we shall content ourselves with the propositional part and omit the
quantiers. If we wanted to treat the quantiers, the idea would be to essen-
tially interpret x and x respectively big & and indexed by the domain
of interpretation of variables ; the precise denition involves considerable bu-
reaucracy for something completely straightforward. The treatment of second-
order quantiers is of course much more challenging and will not be explained
here. See for instance [12].
Once we decided to ignore exponentials and quantiers, everything is ready to
interpret formulas of MALL : more precisely, if we assume that the atomic
propositions p, q, r, . . . of the language have been interpreted by coherent spaces
p

, q

, r

, . . . , then any formula A of the language is interpreted by a well-

dened coherent space A

; moreover this interpretation is consistent with the

denitions of linear negation and implication (i.e. A

= A

, (A B)

=
A

). It remains to interpret sequents ; the idea is to interpret

(= A
1
, . . . , A
n
) as A

1
&

&
A

n
. More precisely
Denition 7
If (= X
1
, . . . , X
n
) is a formal sequent made of coherent spaces,
then the coherent space is dened by
1. [ [ = [X
1
[ [X
n
[ ; we use the notation x
1
. . . x
n
for the atoms
of .
2. x
1
. . . x
n
y
1
. . . y
n
i x
i
y
i
.
If (= A
1
, . . . , A
n
) is a sequent of linear logic, then

will be
the coherent space A

1
, . . . , A

n
.
The next step is to interpret proofs ; the idea is that a proof of will
be interpreted by a clique

. In particular (since sequent calculus is

eventually about proofs of singletons A) a proof of A is interpreted
by a clique of A

i.e. a clique in A

.
30 Jean-Yves Girard
Denition 8
1. The identity axiom A, A

of linear logic is interpreted by the set

xx ; x [A

[.
2. Assume that the proofs of , A and of A

, have been
interpreted by cliques

and

in the associated coherent spaces ; then

the proof of , obtained by means of a cut rule between and
is interpreted by the set

= xx

; z (xz

zx

).
3. Assume that the proof of has been interpreted by a clique

, and that is obtained from by an exchange rule (permutation

of ); then

is obtained from

by applying the same permutation

= (x) ; x

.
All the sets constructed by our denition are cliques ; let us remark that in
the case of cut, the atom z of the formula is uniquely determined by x and x

.
Denition 9
1. The axiom 1 of linear logic is interpreted by the clique 0 of 1 (if
we call 0 the only atom of 1).
2. The axioms , of linear logic are interpreted by void cliques (since
has an empty web, the spaces ( , )

have empty webs as well).

3. If the proof of , comes from a proof of by a falsum
rule, then we dene

= x0 ; x

.
4. If the proof of , A
&
B comes from a proof of , A, B by
a par rule, we dene

= x(y, z) ; xyz

.
5. If the proof of , AB, comes from proofs of , A and
of B, by a times rule, then we dene

= x(y, z)x

; xy

zx

.
6. If the proof of , A B comes from a proof of , A by a
left plus rule, then we dene

= x(y, 0) ; xy

; if the proof of
, AB comes from a proof of , B by a right plus rule, then
we dene

= x(y, 1) ; xy

.
7. If the proof of , A&B comes from proofs of , A and of
, B by a with rule, then we dene

= x(y, 0) ; xy

x(y, 1) ; xy

.
Observe that (4) is mainly a change of bracketing, i.e. does strictly nothing ;
if [A[ [B[ = then one can dene A&B, AB as unions, in which case (6)
is read as

in both cases, and (7) is read

.
It is of interest (since this is deeply hidden in Denition 9) to stress the relation
between linear implication and linear maps :
Linear logic : its syntax and semantics 31
Denition 10
Let X and Y be coherent spaces ; a linear map from X to Y consists in
a function F such that
1. if a X then F(a) Y ,
2. if

b
i
= a X then F(a) =

F(b
i
),
3. if a b X, then F(a b) = F(a) F(b).
The last two conditions can be rephrased as the preservation of disjoint
unions.
Proposition 1
There is a 1-1 correspondence between linear maps from X to Y and
cliques in X Y ; more precisely
to any linear F from X to Y , associate Tr(F) X Y (the trace of
F)
Tr(F) = (x, y) ; y F(x) ,
to any A X Y associate a linear function A() from X to Y
if a X, then A(a) = y ; x a (x, y) A.
Proof. The proofs that Tr(A()) = A and Tr(F)() = F are left to the
reader. In fact the structure of the space X Y has been obtained so as to
get this property and not the other way around. 2
2.2.5 Exponentials
Denition 11
Let X be a coherent space ; we dene /(X) to be the free commutative
monoid generated by [X[. The elements of /(X) are all the formal ex-
pressions [x
1
, . . . , x
n
] which are nite multisets of elements of [X[. This
means that [x
1
, . . . , x
n
] is a sequence in [X[ dened up to the order. The
dierence with a subset of [X[ is that repetitions of elements matter. One
easily denes the sum of two elements of /(X) :
[x
1
, . . . , x
n
] + [y
1
, . . . , y
n
] = [x
1
, . . . , x
n
, y
1
, . . . , y
n
], and the sum is gener-
alized to any nite set. The neutral element of /(X) is written [ ].
If X is a coherent space, then !X is dened as follows :
[!X[ = [x
1
, . . . , x
n
] /(X) ; x
i

x
j
for all i and j,

[x
i
]

[y
j
] [mod !X] i x
i

y
j
for all indices i and j.
32 Jean-Yves Girard
If X is a coherent space, then ?X is dened as follows :
[?X[ = [x
1
, . . . , x
n
] /(X) ; x
i

x
j
for all i and j,

[x
i
]

[y
j
] [mod ?X] i x
i
y
j
for some pair of indices i and j.
Among remarkable isomorphisms let us mention
De Morgan equalities : (!X)

=?(X

) ; (?X)

=!(X

) ;
the exponentiation isomorphisms : !(X&Y ) (!X) (!Y ) ; ?(X Y )
(?X)
&
(?Y ), together with the particular cases ! 1 ; ?0 .
Denition 12
1. Assume that the proof of ?, A has been interpreted by a clique

; then the proof of ?, !A obtained from by an of course rule

is interpreted by the set

= (x
1
+ + x
k
)[a
1
, . . . , a
k
] ; x
1
a
1
, . . . , x
k
a
k

.
About the notation : if ? is ?B
1
, . . . , ?B
n
then each x
i
is x
1
i
, . . . , x
n
i
so
x
1
+ +x
k
is the sequence x
1
1
+ +x
1
k
, . . . , x
n
1
+ +x
n
k
; [a
1
, . . . , a
k
]
refers to a multiset. What is implicit in the denition (but not obvious)
is that we take only those expressions (x
1
+ + x
k
)[a
1
, . . . , a
k
] such
that x
1
+ + x
k
? (this forces [a
1
, . . . , a
k
] [!A[).
2. Assume that the proof of has been interpreted by a clique

;
then the proof of , ?A obtained from by a weakening rule is
interpreted by the set

= x[ ] ; x

.
3. Assume that the proof of , ?A, ?A has been interpreted by a
clique

; then the proof of , ?A obtained from by a contraction

rule is interpreted by the set

= x(a + b) ; xab

b.
4. Assume that the proof of , A has been interpreted by a clique

; then the proof of , ?A obtained from by a dereliction rule

is interpreted by the set

= x[a] ; xa

.
2.2.6 The bridge with intuitionism
First the version just given for the exponentials is not the original one, which
was using sets instead of multisets. The move to multisets is a consequence
of recent progress on classical logic [13] for which this replacement has deep
consequences. But as far as linear and intuitionistic logic are concerned, we
can work with sets, and this is what will be assumed here. In particular /(X)
will be replaced by the monoid of nite subsets of X, and sum will be replaced
by union. The web of !X will be the set X
fin
of all nite cliques of X.
Linear logic : its syntax and semantics 33
Denition 13
Let X and Y be coherent spaces ; a stable map from X to Y is a function
F such that
1. if a X then F(a) Y ,
2. assume that a =

b
i
, where b
i
is directed with respect to inclusion,
then
F(a) =

F(b
i
),
3. if a b X, then F(a b) = F(a) F(b).
Denition 14
Let X and Y be coherent spaces ; then we dene the coherent space
X Y as follows :
[X Y [ = X
fin
[Y [,
(a, y)

(a

, y

) i (1) and (2) hold :

1. a a

X y

,
2. a a

X a ,= a

y y

.
Proposition 2
There is a 1-1 correspondence between stable maps from X to Y and
cliques in X Y ; more precisely
1. to any stable F from X to Y , associate Tr(F) X Y (the trace of
F)
Tr(F) = (a, y) ; a X y F(a) a

a (y F(a

) a

= a)
2. to any A X Y , associate a stable function A( ) from
X to Y
if a X, then A(a) = y ; b a ((b, y) A).
Proof. The essential ingredient is the normal form theorem below. 2
Theorem 3
Let F be a stable function from X to Y , let a X, let y F(a) ; then
1. there exists a
0
a, a
0
nite such that y F(a
0
),
2. if a
0
is chosen minimal w.r.t. inclusion, then it is unique.
34 Jean-Yves Girard
Proof. (1) follows from a =

a
i
, the directed union of its nite subsets ;
z F(

a
i
) =

F(a
i
) hence z F(a
i
) for some i.
(2) : given two solutions a
0
, a
1
included in a, we get z F(a
0
) F(a
1
) =
F(a
0
a
1
) ; if a
0
is minimal w.r.t. inclusion, this forces a
0
a
1
= a
0
, hence
a
0
a
1
. 2
This establishes the basic bridge with linear logic, since X Y is strictly the
same thing as !X Y (if we use sets instead of multisets). In fact one can
translate intuitionistic logic into linear logic as follows :
p

:= p (p atomic),
(A B)

:= !A

,
(A B)

:= A

&B

,
(x A)

:= x A

,
(A B)

:= !A

!B

,
(x A)

:= x !A

,
(

A)

:= !A

0.
and prove the following result: A is intuitionistically provable i !

(i.e. ?

, A

) is linearily provable. The possibility of such a faithful

translation is of course a major evidence for linear logic, since it links it with
intuitionistic logic in a strong sense. In particular linear logic can at least be
accepted as a way of analysing intuitionistic logic.
2.2.7 The bridge with classical logic
Let us come back to exponentials ; the space !X is equipped with two maps :
c !X (!X!X) w !X 1
corresponding to contraction and weakening. We can see these two maps as
dening a structure of comonoid : intuitively this means the contraction map
behaves like a commutative/associative law and that the weakening map be-
haves like its neutral element. The only dierence with a usual monoid is that
the arrows are in the wrong direction. A comonoid is therefore a triple (X, c, w)
satisfying conditions of (co)-associativity, commutativity and neutrality. There
are many examples of monoids among coherent spaces, since monoids are closed
under , and existential quantication (this means that given monoids, the
above constructions can canonically be endowed with monoidal structures).
Let us call them positive correlation spaces.
Dually, spaces ?X are equipped with maps :
Linear logic : its syntax and semantics 35
A B A B A B A B

A x A x A
+1 +1 +1 +1 1 1 1 +1
1 +1 +1 1 +1 +1 1 +1
+1 1 +1 1 1
1 1 1 1 1
Table 1: Polarities for classical connectives.
c (?X
&
?X)?X w ?X
enjoying dual conditions, and that should be called cocomonoids, but we
prefer to call them negative correlation spaces
10
. Negative correlation spaces
are closed under
&
,& and universal quantication.
The basic idea to interpret classical logic will be to assign polarities to for-
mulas, positive or negative, so that a given formula will be interpreted by a
correlation space of the same polarity. The basic idea behind this assignment
is that a positive formula has the right to structural rules on the left and a
negative formula has the right to structural rules on the right of sequents. In
other terms, putting everything to the right, either A or A

has structural
rules for free. A classical sequent , with the formulas in positive
and the formulas in negative is interpreted in linear logic as ?, : the
symbol ? in front of is here to compensate the want of structural rule for
positive formulas.
This induces a denotational semantics for classical logic. However, we eas-
ily see that there are many choices (using the two conjunctions and the two
exponentials) when we want to interpret classical conjunction, similarly for
disjunction, see [8], this volume. However, we can restrict our attention to
choices enjoying an optimal amount of denotational isomorphisms. This is the
reason behind the tables shown on next page.
It is easily seen that in terms of isomorphisms, negation is involutive, con-
junction is commutative and associative, with a neutral element V of polarity
+1, symmetrically for disjunction. Certain denotational distributivities /
or / are satised, depending on the respective polarities.
Polarities are obviously a way to cope with the basic undeterminism of clas-
sical logic, since they operate a choice between the basic protocols of cut-
10. The dual of a comonoid is not a monoid
36 Jean-Yves Girard
A B A B A B A B

A x A x A
+ 1 +1 A B A B A?B A

x ?A x A
1 +1 !A B A
&
?B A

B A

x A x !A
+ 1 1 A!B ?A
&
B A B
1 1 A & B A
&
B !A B
Table 2: Classical connectives : denition in terms of linear logic.
elimination. However, this is still not enough to provide a deterministic version
of Gentzens classical calculus LK. The reason lies in the fact that the rule of
introduction of conjunction is problematic : from cliques in respectively ?X
and ?Y , when both X and Y are positive, there are two ways to get a clique
in ?(X Y ). This is why one must replace LK with another calculus LC, see
[13] for more details, in which a specic positive formula may be distinguished.
LC has a denotational semantics, but the translation from LK to LC is far
from being deterministic. This is why we consider that our approach is still
not absolutely convincing . . . typically one cannot exclude the existence of a
non-deterministic denotational semantics for classical logic, but God knows
how to get it !
LC is indeed fully compatible with linear logic : it is enough to add a new
polarity 0 (neutral) for those formulas which are not canonically equipped
with a structure of correlation space. The miracle is that this combination of
classical with intuitionistic features accommodates intuitionistic logic for free,
and this eventually leads to the system LU of unied logic, see [14].
2.3 Geometry of interaction
At some moment we indicated an electronic analogy ; in fact the analogy was
good enough to explain step (1) of cut-elimination (see subsection 1.3.6 by the
fact that an extension cord has no action (except perhaps a short delay, which
corresponds to the cut-elimination step). But what about the other links ?
Let us rst precise the nature of our (imaginary) plugs ; there are usually
several pins in a plug. We shall restrict ourselves to one-pin plugs ; this does
not contradict the fact that there may be a huge variety of plugs, and that the
only allowed plugging is between complementary ones, labelled A and A

.
Linear logic : its syntax and semantics 37
The interpretation of the rules for and
&
both use the following well-
known fact : two pins can be reduced to one (typical example : stereophonic
broadcast).
-rule : from units , with respective interfaces , A and , B , we
can built a new one by merging plugs A and B into another one (labelled
A B) by means of an encoder.

A
AB
B

&
-rule : from a unit with an interface C, D, , we can built a new
one by merging plugs C and D into a new one (labelled C
&
D) by means
of an encoder :
C
D
.
.
.
.
.

C
&
D
.
To understand what happens, let us assume that C = A

, D = B

; then
A

&
B

= (A B)

, so there is the possibility of plugging. We therefore

obtain
.
.
.
.
.
.

A

&
B

AB

A
B

But the conguration

is equivalent to (if the coders are the same)
38 Jean-Yves Girard
and therefore our plugging can be mimicked by two pluggings
B

B
.
.
.
.
.
.

A

If we interpret the encoder as - or

&
-link, according to the case, we get
a very precise modelization of cut-elimination in proof-nets. Moreover, if we
remember that coding is based on the development by means of Fourier series
(which involves the Hilbert space) everything that was done can be formulated
in terms of operator algebras. In fact the operator algebra semantics enables
us to go beyond multiplicatives and quantiers, since the interpretation also
works for exponentials. We shall not go into this, which requires at least some
elementary background in functional analysis ; however, we can hardly resist
mentioning the formula for cut-elimination
EX(u, ) := (1
2
)u(1 u)
1
(1
2
)
which gives the interpretation of the elimination of cuts (represented by )
in a proof represented by u. Termination of the process is interpreted as the
nilpotency of u, and the part u(1 u)
1
is a candidate for the execution.
See [15], this volume, for more details. One of the main novelties of this paper
is the use of dialects, i.e. data which are dened up to isomorphism. The dis-
tinction between the two conjunctions can be explained by the possible ways
of merging dialects : this is a new insight in the theory of parallel computation.
Geometry of interaction also works for various -calculi, for instance for pure
-calculus, see [7, 26]. It has also been applied to the problem of optimal
reduction in -calculus, see [20].
Let us end this chapter by yet another refutation of weakening and contraction :
1. If we have a unit with interface , it would be wrong to add another plug
A ; such a plug (since we know nothing about the inside of the unit) must
be a mock plug, with no actual connection with the unit . . . Imagine a plug
on which it is written danger, 220V, you expect to get some result if you
plug something with it : here nothing will happen !
2. If we have a unit with a repetitive interface , A, A, it would be wrong
to merge the two similar plugs into a single one : in real life, we have such
a situation with the stereophonic output plugs of an amplier, which have
exactly the same specication. There is no way to merge these two plugs
Linear logic : its syntax and semantics 39
into one and still respect the specication. More precisely, one can try to
plug a single loudspeaker to the two outputs plugs simultaneously ; maybe it
works, maybe it explodes, but anyway the behaviour of such an experimental
plugging is not covered by the guarantee . . .
2.4 Game semantics
Recently Blass introduced a semantics of linear logic, see [5], this volume. The
semantics is far from being complete (i.e. it accepts additional principles), but
this direction is promising.
Let us forget the state of the art and let us focus on what could be the general
pattern of a convincing game semantics.
2.4.1 Plays, strategies etc.
Imagine a game between two players I and II ; the rule determines which is
playing rst, and it may happen that the same player plays several consecutive
moves. The game eventually terminates and produces a numerical output for
both players, e.g. a real number. There are some distinguished outputs for
I for which he is declared to be the winner, similarly for II, but they cannot
win the same play. Let us use the letter for a strategy for player I, and the
letter for a strategy for II. We can therefore denote by the resulting
play and by < , > the output. The idea is to interpret formulas by games
(i.e. by the rule), and a proof by a winning strategy. Typically linear negation
is nothing but the interchange of players etc.
2.4.2 The three layers
We can consider three kinds of invariants :
1. Given the game A, consider all inputs for I of all possible plays : this vaguely
looks like a phase semantics (but the analogy is still rather vague) ;
2. Given the game A and a strategy for I consider the set [ [ of all plays
, when varies among all possible strategies for II. This is an analogue
of denotational semantics : we could similarly dene the interpretation [ [
of a strategy for II and observe that [ [ [ [= (this is analogue
to the fact that a clique in X and a clique in X

intersect in at most one

point) ;
3. We could concentrate on strategies and see how they dynamically combine :
this is
analogous to geometry of interaction.
Up to the moment this is pure science-ction. By the way we are convinced
that although games are a very natural approach to semantics, they are not
40 Jean-Yves Girard
primitive, i.e. that the game is rather a phenomenon, and that the actual
semantics is a more standard mathematical object (but less friendly). Any-
way, whatever is the ultimate status of games w.r.t. logic, this is an essential
intuition : typically game semantics of linear logic is the main ingredient in
the recent solution of the problem of full abstraction for the language PCF,
see [1].
2.4.3 The completeness problem
The main theoretical problem at stake is to nd a complete semantics for (rst
order) linear logic. Up to now, the only completeness is achieved at the level of
provability (by phase spaces) which is rather marginal. Typically a complete
game semantics would yield winning strategies only for those formulas which
are provable. The diculty is to nd some semantics which is not contrived (in
the same way that the phase semantics is not contrived : it does uses, under
disguise, the principles of linear logic).
A non-contrived semantics for linear logic would denitely settle certain general
questions, in particular which are the possible rules. It is not to be excluded
that the semantics suggests tiny modications of linear rules (e.g. many se-
mantics accept the extra principle
A B A
&
B, known as mix), (and which can be written as a structural
rule), or accepts a wider spectrum of logics (typically it could naturally be
non-commutative, and then set up the delicate question of non-commutativity
in logic). Surely it would give a stable foundation for constructivity.
Acknowledgements
The author is deeply indebted to Daniel Dzierzgowski and Philippe de Groote
for producing L
a
T
E
X versions of a substantial part of this text, especially g-
ures. Many thanks also to Yves Lafont for checking the nal version.
Linear logic : its syntax and semantics 41
BIBLIOGRAPHY
[1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for
pcf (extended abstract). In Masami Hagiya and John C. Mitchell, ed-
itors, Theoretical Aspects of Computer Software. International Sympo-
sium, TACS 94, Sendai, Japan. Springer Verlag, April 1994. Lecture
Note in Computer Science 789.
[2] V. M. Abrusci. Non-commutative proof-nets. In this volume, 1995.
[3] J.-M. Andreoli and R. Pareschi. Linear objects: logical processes with
built-in inheritance. New Generation Computing, 9(34):445473, 1991.
[4] A. Asperti. A logic for concurrency. Technical report, Dipartimento di
Informatica, Pisa, 1987.
[5] A. Blass. A game semantics for linear logic. Annals of Pure and Applied
Logic, 56:183220, 1992.
[6] R. Blute. Linear logic, coherence and dinaturality. Theoretical Computer
Science, 93:341, 1993.
[7] V. Danos. La logique lineaire appliquee ` a letude de divers processus de
normalisation et principalement du -calcul. PhD thesis, Universite Paris
VII, 1990.
[8] V. Danos, J.-B. Joinet, and H. Schellinx. LKQ and LKT : sequent calculi
for second order logic based upon dual linear decompositions of classical
implication. In this volume, 1995.
[9] V. Danos and L. Regnier. The structure of multiplicatives. Archive for
Mathematical Logic, 28:181203, 1989.
[10] T. Ehrhard. Hypercoherences : a strongly stable model of linear logic. In
this volume, 1995.
[11] C. Fouquere and J. Vauzeilles. Inheritance with exceptions : an attempt
at formalization with linear connectives in unied logic. In this volume,
1995.
[12] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1102, 1987.
[13] J.-Y. Girard. A new constructive logic : classical logic. Mathematical
structures in Computer Science, 1:255296, 1991.
[14] J.-Y. Girard. On the unity of logic. Annals of Pure and Applied Logic,
59:201217, 1993.
42 Jean-Yves Girard
[15] J.-Y. Girard. Geometry of interaction III : accommodating the additives.
In this volume, 1995.
[16] J.-Y. Girard. Light linear logic. in preparation, 1995.
[17] J.-Y. Girard. Proof-nets : the parallel syntax for proof-theory. In Logic
and Algebra, New York, 1995. Marcel Dekker.
[18] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and types, volume 7 of
Cambridge tracts in theoretical computer science. Cambridge University
Press, 1990.
[19] J.-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A mod-
ular approach to polynomial time computability. Theoretical Computer
Science, 97:166, 1992.
[20] G. Gonthier, M. Abadi, and J.-J. Levy. The geometry of optimal lambda-
reduction. In ACM Press, editor, POPL92, Boston, 1992. Birkh auser.
[21] Y. Lafont. The linear abstract machine. Theoretical Computer Science,
59:95108, 1990.
[22] Y. Lafont. From proof-nets to interaction nets. In this volume, 1995.
[23] J. Lambek. Bilinear logic in algebra and linguistics. In this volume, 1995.
[24] P. Lincoln. Deciding provability of linear logic fragments. In this volume,
1995.
[25] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for
propositional linear logic. Annals of Pure and Applied Logic, 56:239311,
1992.
[26] Laurent Regnier. Lambda-Calcul et Reseaux. Th`ese de doctorat, Univer-
site Paris 7, 1992.
[27] D.N. Yetter. Quantales and non-commutative linear logic. Journal of
Symbolic Logic, 55:4164, 1990.