Re: Light logics vs. CoS

>  > Did you try the naive deep versions of these rules, i.e.:
>>
>>    S[R,T]     S[R]
>>    --------   -----
>>    S[?R,!T]   S[!R]
>>
>
>They were my first guess. Unfortunately, they are definately more
>powerful than the non-deep ones. For example, consider the
>sequent |- a,!(a^\bot). It cannot be proved in LAL
>(nor in MELL?), but you can prove it using the second
>naive deep rule (correct me if I am wrong):
>
>       1
>   -----------
>   [a,[a^\bot]]
>   -------------
>   [a,[!(a^\bot)]]

What about

     S{![R,T]}
    ----------- ,
    S{![!R,?T]}

together with !1 = 1, of course?

I didn't check at all, but my guess is about having a CoS system that 
proves !R iff LAL proves R.

>I have another question to all the Frogs here: did you
>try to formulate the approximation theorem for linear
>logic (see Troelstra's Lectures on Linear Logic) in
>the framework of CoS? Obviously, it continues to hold
>(it talks about provability). My guess, however, is
>the following: using cut atomicity, you can make it
>working on proofs rather than formulae...

I know the approximation theorem but still don't understand what you 
mean. In approximation, you substitute modalities with certain 
non-modal formulas, and the theorem tells you that you can always do 
it. What has this to do with proofs, and why may atomic cuts be 
relevant?

-Alessio