Re: Light logics vs. CoS

Lutz:

I am not convinced about

>     S[R,T]
>    --------
>    S[?R,!T]

Consider, for example, the sequent

  |- a^\bot,?a^\bot,!(a\otimes a)

The corresponding structure is provable
by way of the naive deep rule above.
However, I cannot figure out a
sequent calculus proof for it...

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

I will post a separate message about the
approximation theorem...

Ugo.