[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.