[Prev][Next][Index][Thread]
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.