Re: (Frogs) Calculus of Structures and substructura

Lutz,

Many thanks for your reply. You mention a lot of very interesting
material (especially De Groote and Lamarche's work). A minor note on
the use of the following rules

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

Michael Moortgat refers to these as type I Grishin interactions. They
constitute one way of extending the basic system without sacrificing
(same-sort) non-associativity and non-commutativity. But we can also
use

(A\\B) * C |- A\\(B*C)
A * (C//B) |- (A*C)//B
(A//B) * C |- (A*C)//B
A * (B\\C) |- B\\(A*C)

(And dually A\(B+C) |- (A\B)+C, etc.)  These rules are referred to by
Moortgat as type IV interactions. But note that we can't have both: if
we add both type I and type IV interactions, we get a partial collapse
into same-sort associativity and -commutativity:

(A*B)*C |- D+E    iff   A*(B*C) |- D+E
(A*B)*C |- D+E    iff   (A*C)*B |- D+E
A*(B*C) |- D+E    iff   B*(A*C) |- D+E

become derivable (and similarly for +), which I think would be
unfortunate if we want to study non-associative, non-commutative
systems. So it would also be an interesting question as to how a
cos-style presentation of the basic system extended with type IV
interactions, but no type I interactions, would look like.


On Thu, Feb 12, 2009 at 6:27 PM, Lutz Strassburger
<[email protected]> wrote:
>
> 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
>
>