Re: (Frogs) Calculus of Structures and substructura

Dear Arno,

You have hit quite an interesting problem. Let me try to answer your 
questions.

On Wed, 11 Feb 2009, Arno Bastenhof wrote:

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

If I understand correctly, then what you have sofar is the basic 
non-associative, non-commutative classical (i.e., non-intuitionistic) 
Lambek calculus. There is a very well written paper on that logic by 
Philipp de Groote and Francois Lamarche:

Classical Non-Associative Lambek Calculus. Studia Logica, 71.1 (2) 
<http://www.loria.fr/~lamarche/papers/DeGrooteLamarche.ps.gz>

In that paper the presentation of the logic is in terms of proof nets and 
the sequent calculus. It is not real "deep inference", but the symmetric 
approach to syntax in that paper gives a spirit of "deepness" and allows 
by the use of polarities to reduce the six connectives to two connectives, 
one par and one tensor. Furthermore,

   B |- A\C    and    A*B |- C     and     A |- C/B

are no longer three different sequents, but the same.

> 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)

Yes. If we add one or more of these axioms, we get what is called 
"Lambek-Grishin calculus".

> 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?

There is nothing written up. But there is some work in progress between 
Francois Lamarche and myself. The basic idea is: start from the sequent 
system by de Groote and Lamarche and add the Grishin axioms as deep 
inference rules. They then behave similar to the switch rule.

One observation is that there are 96 instead of Grishin's 16 different 
axioms that we can add.

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

This is indeed the problem. In the paper by de Groote and Lamarche this 
has solved by polarizing the connectives.

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

This is an interesting possibility, and as far as I know it has not 
been explored so far.

> 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?

As far as I know there is only this unfinished business that I mentioned 
above, and it is not really within the calculus of structures.

One has to keep in mind that some of the nice properties of the system for 
classical and linear logic that you mention are due to the properties of 
the logics themselves. Thus, for a different logic, one should expect 
different properties.

It also depends on the structures involved: In classical and linear
logic, sequents are multisets, and formulas are rooted trees. In
tradidtional associative Lambek calculus, sequents are cyclic orders. In
the non-associative, non-commutative classical Lambek calculus that we
discuss here, sequents are unrooted trees, whose leaves are filled with
formulas. It is not obvious how to present such a structure in the 
Calculus of Structures.

So, there are quite a few open research questions here that need to be 
tackled.

Kind regards,
Lutz