Re: Structural Rules and Exponentials
This is an answer to the message by Maurizio Castellan sent from
firstname.lastname@example.org (Thu, 2 Feb 95).
The fact that the promotion rule in ILL (or in LL) cannot be replaced by
A |- B A |- 1 A |- A \otimes A
A |- !B
was already known. A related fact is that, if we have two exponentials ! and !'
with the same rules in the syntax, then it is impossible to relate !A with !'A.
In other words, ! is not determined by its rules.
Also, in coherence semantics, there are several possible definitions for
exponentials (see ). One of them (not the original one) uses multisets (see
): It is a cofree (cocommutative) comonoid in the sense of , which is the
categorical analogue of the above rule.
It is not so easy to give a general categorical formulation of exponentials.
The notion given in  is enough to get a cartesian closed coKleisli category,
but not for modeling linear logic. I think that the correct formulation has
been given by G.M. Bierman.
 Y. Lafont, (1988). The linear abstract machine. Theoretical Computer
Science 59, pp. 157-180 (corrections Ibidem 62, pp. 327-328).
 R. Seely, (1989). Linear logic, *-autonomous categories and cofree
 J.Y. Girard, (1991). A new constructive logic: classical logic.
Mathematical structures in Computer Science, 1(3), pp. 255-296.
 M. Quatrini, (1995). S\'emantique coh\'erente des exponentielles : de la
logique lin\'eaire \`a la logique classique, Th\`ese de doctorat, Universit\'e