# Structural Rules and Exponentials



Is the following result already known ?

There exist two formulas  A and B of  CLL s.t. :
\Gamma   |- \Delta
----------------------- (L,W)
\Gamma , A |- \Delta

\Gamma , A, A  |- \Delta=
--------------------------- (L,C)
\Gamma , A |- \Delta

\Gamma   |- \Delta
----------------------- (R,W)
\Gamma  |- \Delta , B

\Gamma  |- B, B, \Delta
-------------------------- (R,C)
\Gamma |- B, \Delta

but

A |- !A is not provable

and

?B |- B is not provable

(i.e. A is not equivalent to !A and B is not equivalent to ?B)

namely :

A:=!(((p -o 1) \otimes p) -o (((p -o 1) \otimes p) \otimes

(( p -o 1) \otimes p))) \otimes (( p -o 1) \otimes p)

B:= nil(A)

The above result holds in ILL as well w.r.t.  (L,W), (L,C) and
formula A.

Some consequences:  If  Q  is an unital quantale (a Girard quantale),
for any a \in Q  let

!_{m}(a)=sup(b \in Q | b <=a, b<=1, b<=b \otimes b)

Yetter in [1] put the following question:
"Is the quantale semantics with "!" interpreted by "!m" complete?"

Now we know that this semantics is incomplete.

--------------------------------

The variant of ILL [2] in which the rule:

!\Gamma |- A
-----------------(R,!)
!\Gamma |- !A

is  replaced by the rule:

A |- B    A |-1   A |- A \otimes A
------------------------------------(R,!)
A |- !B

is not equivalent to ILL.

Maurizio Castellan,
Dept. Math. University of Siena
castellan@sivax.cineca.it
----------------------------------
[1] D. Yetter, (1990). Quantales and (non-commutative) linear logic,
The Journal of Symbolic Logic 55 ,  pp.41-64.
[2] Y. Lafont , (1988). The linear abstract machine. Theoretical
Computer Science 59 ,  pp.157-180.