[Prev][Next][Index][Thread]
Re: Exponentials in linear logic

To: Clemens Cap <cap@ifi.unizh.ch>

Subject: Re: Exponentials in linear logic

From: girard@lmd.univmrs.fr (JeanYves GIRARD)

Date: Tue, 13 Sep 94 14:17:10 +0200

Approved: types@dcs.gla.ac.uk
Answer to Clemens H. CAP (mail of August 1st)
The question of duality of ! and ? is exactly the same as the
question of the unicity of !. By nature ! cannot be unique :
1st reason : ! controls infinity in logic ; we get usual infinity by
means of the familiar rules, but another choice of rules can yield
weaker notions of infinity, eg polytime. In this respect, there is no
a priori unicity of !, and this is far from being a weakness...
2nd reason : just write twice the same set of rules (eg in an
intuitionistic style) for ! and say $ ; it will be impossible to
prove the equivalence between !A and $A. If we want to prove $A o !A
then we must allow contexts $Gamma,!Delta in the !Srule. In general
we can handle several !, partially ordered, etc. But one should use
this latter possibility with extreme care : multimodal logics are
close relatives of nonmonotonic "logics".

JeanYves GIRARD
Directeur de Recherche
CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9
<girard@lmd.univmrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)