Re: Light logics vs. CoS

Ugo, I only found very little time to work on that: I think you're 
right, my proposal doesn't work and right now I have no constructive 
suggestion. I hope I'll find some time to work on this. For now, I go 
on holiday!   -Alessio


At 9:47 AM +0200 11.6.04, Ugo Dal_Lago wrote:
>  > 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.