Re: Light logics vs. CoS

On Wednesday 09 June 2004 09:11, Ugo Dal_Lago wrote:
> 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)]]

OK. the deep version of 
  R
 ---
 !R
is stronger than the shallow one. But the case is not yet lost:

First we should inspect the other rule. Do we observe the same phenomenon, or 
do deep and shallow version have the same strength (which would be my guess).
If 
    S[R,T]   
   --------  
   S[?R,!T]  
is ok, then we can replace
  R
 ---
 !R
by 
  S{1}
  -----
  S{!1}
which is deep and should solve the problem.

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

Unfortunately, I have no access to Troelstra's Lectures on Linear Logic. Can 
you quickly recall the approximation theorem?

-Lutz