[Prev][Next][Index][Thread]

Structural Rules





Recently I happened to come across the paper: "Structural Rules and Quantales" 
by M. Castellan and M. Piazza.
The main result of this paper is the following: Call a formula $A$ of $LL_{m}$
a (W,L) formula if $A,\Gamma\Rightarrow\Delta$ is provable whenever
$\Gamma\Rightarrow\Delta$ is, and call it a (C,L) formula if 
$A,\Gamma\Rightarrow\Delta$ is provable whenever $A,A,\Gamma\Rightarrow\Delta$
is. Then $A$ is both a (W,L) and a (C,L) formula iff it is equivalent in
$LL_{m}$ to the multiplicative constant 1. This result is proved using
an interesting (but relatively complicated) semantic argument. 

  It might be interesting to note the following generalizations and
stronger results (which have all simple, strictly proof-theoretical proofs):

1. $A$ is a (C,L) formula of $LL_{m}$ iff $A$ is a theorem of $LL_{m}$. 
2. This remains the case if we add either the additive operators (but not 
   the additive constants), or the mix rule, or both. 
3. More generally, there is n>1 s.t. A->A^{n} is provable in any of these 4 
   systems iff $A$ is a theorem of that system (where A^{n} means repeated
   tensor multiplication of $A$).
4. In $LL_{ma}$ (with the additive constants) $A$ is a (C,L) formula (more
   generally: there is n>1 s.t. A->A^{n} is provable) iff 
   either $A$ is provable or $A$ is equivalent (in $LL_{ma}$)
   to the additive constant 0 (and $A$ has both properties if it is 
   equivalent to either 1 or 0). Again, this remains true if we add mix.
5. The claim in 4 holds also for multiplicative-additive affine logic.