(Frogs) Calculus of Structures and substructural lo

While reading literature on the calculus of structures, primarily on
its applications to classical and linear logic, I have started to
wonder as to whether similar systems could be derived for
substructural logics. The presentations of classical and linear logic
enjoy some very interesting properties, although their strong reliance
on the presence of special objects and structural rules seems to me to
make it difficult to extend these ideas to the substructural case.
Note, however, that I am definitely not an expert here (far from): I
am actually a student of linguistics, with my interest in proof theory
mainly deriving from type-logical grammars. But let me give an example
of a particular logic that I am interested in myself (adopting for its
presentation a format much like Lambek's deductive systems). Given
some set of propositional variables, complex formulae are derived
using binary connectives * (tensor), + (par), / (right implication), \
(left implication), // (right co-implication / subtraction) and \\
(left subtraction). Sequents are of the form A |- B, for A and B
formulas. Next to the preorder axioms on derivability:

(Refl) A |- A
(Trans) from A |- B and B |- C, conclude A |- C

We have the following monotonicity rules:

( *  ) from A |- B and C |- D, conclude A*C |- B*D
( +  ) from A |- B and C |- D, conclude A+C |- B+D
( \  ) from A |- B and C |- D, conclude D\A |- C\B
( /  ) from A |- B and C |- D, conclude A/D |- B/C
( \\ ) from A |- B and C |- D, conclude D\\A |- C\\B
( \\ ) from A |- B and C |- D, conclude A//D |- B//C

And finally, (*,/,\) is a residuated triple, with (+,\,/) being a
co-residuated triple

(Res)  B |- A\C   iff   A*B |- C    iff   A |- C/B
(CoRes)  A\\C |- B    iff   C |- A+B   iff   C//B |- A

The resulting logic is also referred to as the Lambek-Grishin calculus
(LG, for short) in the literature. Note that neither the tensor nor
the par is associative or commutative, and we don't have any rules of
mixed associativity or commutativity. That is, we do *not* have:

(A+B)*C |- A+(B*C)
(A+B)*C |- (A*C)+B
A*(B+C) |- (A*B)+C
A*(B+C) |- B+(A*C)

So something like the switch rule wouldn't immediately be valid here.
My question now is: can LG also be given a presentation in the
calculus of structures similar to (and enjoying all the nice
properties of) those of classical and linear logic?

Most instantiations of the calculus of structures for classical and
linear logic I have seen so far draw inspiration from Gentzen-Schutte
systems, relying on the DeMorgan laws and 'doing away' with the
implication. Although we do not have an explicit negation in the
particular case of LG, we could still try something similar by working
with polarities. But if we wish to do away with both implications as
well as subtractions, we cannot suffice by polarizing only the atomic
formulas. For instance (writing p for positive atomic formulae and ~p
for negative atomic formulae), we would be able to interpret
(p+(~p*q))+p both as ((q\p)//p)\p  (when interpreting (p+(~p*q))
negatively) and  (p+(p\\q))+p (when interpreting (p+(~p*q))
positively). And although we do have derivability of:

q+p |- (p+(p\\q))+p

in LG, we do *not* have derivability of:

q+p |- ((q\p)//p)\p

So if we are going to work with polarities, defining implications and
subtractions in terms of tensors, pars and the polarities, it would
seem that we would also have to explicitly polarize *sub*formulas. But
any more than this I have not yet managed to find. If we work with
formulae generated solely by the tensor and par, with explicit
polarization of all subformulas, one could wonder whether any
specialized instantiations of the switch rule (that is, with certain
specific polarities) might be valid in LG. But so far I have found
nothing here that seems to be particularly useful. Of course, we could
also pursue a slightly different presentation of LG by adopting,
instead of (Res) and (CoRes):

a*(a\b) |- b
a |- b\(b*a)
b |- (b//a)+a
(a+b)//b |- a

And similarly for / and \\. In this case, we could formulate a deep
inference style presentation of LG similar to the system found in "An
Algorithmic Interpretation of a Deep Inference System" by Brunnler and
McKinley. But this seems to me to be a vastly different kind of
presentation (in terms of the types of rules adopted) than those
devised for classical and linear logic. So, coming back to my
question: has there already been any work done on analyzing (or that
suggest a way of analyzing) substructural logics of the type presented
here (LG) within the calculus of structures?


Regards,

Arno Bastenhof