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


    A |- !A is not provable 


    ?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
             !\Gamma |- !A

is  replaced by the rule:  

   A |- B    A |-1   A |- A \otimes A
                  A |- !B

is not equivalent to ILL.

       Maurizio Castellan, 
 Dept. Math. University of Siena 
[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.