Re: (Frogs) Calculus of Structures and substructura

> Are you saying that the cos-style rules (as I wrote them) are unsound
> for your logic? That there is no combination of your numerous
> connectives to make them sound

That seems to be the case. For instance, take

A ^ (B -> C)
-----------------
(A -> B) -> C

Or, rewritten using the connectives of LG:

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

Using residuation, we can bring (A\B) over to the other side of the turnstile:

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

But now we need to rearrange the antecedent into (A * (A\B)) * (B\C),
for which we need associativity and commutativity (which we don't
generally have in LG). Of course, we can also try other formulations,
like

A * (B\C) |- C/(B/A)  or   A * (B\C) |- (B/A)\C  or  A*(B\C) |- C/(A\B), etc.

But none of these are provable in LG (or, more generally, Lambek-style
calculi) without assuming associativity and/or commutativity of the
tensor. Note that the middle one ( A* (B\C) |- (B/A)\C, or, dually,
(C/B)*A |- C/(A\B) ) only requires associativity, so maybe that one
could still be used for a cos style presentation of the associative
(non-commutative) Lambek calculus. As for the more general rule

(A -> B) ^ ( C -> D)
--------------------------
(B -> C) -> (A -> D)

The closest sequent that I can find the provability of which only
requires associativity is

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

But we're not there yet: we haven't yet validated the i-up rule. For
that we could assume something like the existence of a unit for the
tensor (which is also not something that we would generally want in
the case of LG).

On Fri, Feb 13, 2009 at 11:34 AM, Kai Brünnler <[email protected]> wrote:
> Arno,
>
>> Regarding the derivation
>> of rules like (A /\ (A -> B)) -> B in cos: if you go the other way
>> around (trying to derive the the cos rules), just having (A /\ (A ->
>> B)) -> B and A -> B -> (B /\ A) won't be enough: you also require the
>> conjunction to be at least associative (and probably also commutative,
>
> Are you saying that the cos-style rules (as I wrote them) are unsound
> for your logic? That there is no combination of your numerous
> connectives to make them sound?
>
> -Kai
>