Re: Light logics vs. CoS

Dear Frogs,

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

Another idea I am trying to explore
consists in introducing another modality
(call it &). The new modality satisfies
the equation 1=&1. There is a new rule

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

However, this seems to be too ad hoc...


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


Ugo.