Re: Light logics vs. CoS

> At 17:32 +0200 10.6.04, Ugo Dal_Lago wrote:
> >  > What about
> >>
> >>       S{![R,T]}
> >>      ----------- ,
> >  >     S{![!R,?T]}
> >>
> >>  together with !1 = 1, of course?
> >
> >I am not able to understand your intuition. If you can freely use
> >this rule, you can build a derivation such as the following:
> >
> >     ![[a,a,a],b]
> >     ----------------
> >     ![![[a,a],a],?b]
> >     ------------------
> >     ![![![a,a],?a],?b]
> >     ------------------
> >     ![![!a,?a,?a],?b]
> >
> >If you map structures to "equivalent" sequents in the usual way, you
> >can prove much more than what you prove in LAL...
>
> No, with my rule the bottommost inference in your example is
> impossible: ![!a,?a,?a] doesn't match ![!R,?T], unless I'm missing
> something.

You are right. The derivation I had in mind was

    ![[a,a,a],b]
    ----------------
    ![![[a,a],a],?b]
    ------------------
    ![![![a,a],?a],?b]
    ------------------
    ![![![!a,?a],?a],?b]

But I still do not understand... What is the LAL sequent
corresponding to the conclusion of this derivation?
Is it obtained by just removing the outer bang (as you
suggest in your previous email)? If you translate structures
into sequents in the same way Lutz does, then your
rule is certainly unsound, because it would correspond
to

|- ?(A^\bot \otimes B^\bot)\par !(!A\par ?B)

which is not provable in LAL.


Ugo.