This is an answer to the message by Maurizio Castellan sent from
marco@nextiac.iac.rm.cnr.it (Thu, 2 Feb 95).
Yves Lafont.
The fact that the promotion rule in ILL (or in LL) cannot be replaced by
A |- B A |- 1 A |- A \otimes A
------------------------------------(R,!)
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 [4]). One of them (not the original one) uses multisets (see
[3]): It is a cofree (cocommutative) comonoid in the sense of [1], 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 [2] 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.
[1] Y. Lafont, (1988). The linear abstract machine. Theoretical Computer
Science 59, pp. 157-180 (corrections Ibidem 62, pp. 327-328).
[2] R. Seely, (1989). Linear logic, *-autonomous categories and cofree
coalgebra.
[3] J.Y. Girard, (1991). A new constructive logic: classical logic.
Mathematical structures in Computer Science, 1(3), pp. 255-296.
[4] M. Quatrini, (1995). S\'emantique coh\'erente des exponentielles : de la
logique lin\'eaire \`a la logique classique, Th\`ese de doctorat, Universit\'e
Aix-Marseille II.