Re: Light logics vs. CoS

Dear Frogs,

> > 3. LIGHT AFFINE LOGIC (LAL, [1])
> >
> > This is a simplification on the original system
> > by Girard. Four modalities are needed, but the
> > interesting one is the usual !, which behaves
> > similarly to ELL but with the following, very
> > strict, constraint on functorial promotion: Gamma
> > can contain at most one formula occurrence. In
> > other words, one replaces functorial promotion by
> >
> >  |- A,B    |- A
> >
> >  -------   -----
> >
> >  |-?A,!B   |- !A
> >
> > Naively, you can translate these two rules into
> > CoS rules
> >
> >  [R,S]     [R]
> >  -------   ----
> >  [?R,!S]   [!R]
> >
> > These rules, however, are not deep!
> > Currently, I am trying to understand whether
> > light affine logic and deep inference
> > are inherently incompatible or not.
>
> 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)]]

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...

Bye.
Ugo.