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.

>  > 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?
>
>I will explain the reason why I believe this to be interesting by way of a
>number of observations:
>
>a. As Alessio pointed out, the approximation theorem allows
>   you to map sequents in a "source" system (namely
>   LL) to sequents in a "target" system (namely MALL) in
>   such a way that *provability* is preserved.
>b. The approximation theorem is originally formulated for full
>   linear logic, but continues to hold in the context of light
>   logics. Moreover, if you have free weakening, you can throw
>   away additives. The target system then becomes MLL.
>c. The way you prove the approximation theorem is an
>   induction on the structure of *cut-free* proofs in the
>   source system. This proof can be turned into an algorithm
>   Approx (from proofs of the source system to proofs in the
>   target system). Studying the complexity of this
>   algorithm is not difficult.
>d. The only reason why Approx cannot work on proofs
>   containing cuts is the possibility of having cut-formulae
>   with modal subformulae. If cuts are constrained to be
>   atomic, Approx works on every proof.
>e. The normalization of an MLL proof is very easy from a
>   computational point of view.
>f. We need an easy and general methodology
>   for studying the complexity of cut-elimination in
>   the context of light logics.

Yes, it looks interesting.

There is a crucial point: in order to `easily' obtain an atomic cut 
in a CoS system, for MELL one needs Lutz's promotion rule:

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

The reason is that this rule (like any core rule) allows for a 
structural induction on principal structures in a cut, leading to 
atomic cuts. The induction needs not be necessarily done with this 
rule, but the point is that one cannot take for granted that cut is 
reducible to atomic form just because one has deep inference. For 
example, the rule I propose doesn't have this property of allowing a 
straightforward structural induction. But the first question is: does 
my rule work?

-Alessio