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.