Re:Paper announcement: CMDL in CoS

Hi,

there is an analogy between the rules rpf and rpp in your paper and 
the rules z in Lutz's paper on linear logic 
<http://www.lix.polytechnique.fr/~lutz/papers/lls-lpar.pdf>, just 
look at:

        mb.[tb.R T]            !(* R T *)
   rpf_ -----------   and   z^ ---------- .
         [R mb.T]                (R !T)

The rules z were the only ones that are not captured by the scheme 
for `subatomic logic' that I discussed in 
<http://cs.bath.ac.uk/ag/p/AG8.pdf> and 
<http://cs.bath.ac.uk/ag/p/AG16.pdf>, and which is:

   b a RU a TV
   ----------- ,
   a b RT b'UV

where a, b and b' are binary relations in prefix form. Now, rpf and 
rpp also fall out of my scheme, because they involve three nested 
logical relations (for example, mb, [] and tb, in rpf).

So, given the analogy, I wonder whether z might be a special case of 
a three-layer rule, and whether it is possible to see also the new 
rules as instances of a more general scheme.

I'm interested in collecting all rule specimens, including those that 
didn't make to the final paper but that `make sense'.

Also, note the mismatch in up and down between your paper and Lutz's.

One more thing: it is true that for many systems we don't have a 
cut-elimination proof which is specific to the calculus of 
structures, and that we have to resort to techniques borrowed from 
other formalisms. However, many of these formalisms can be 
represented inside the calculus of structures, for example the 
sequent calculus and hypersequents.

So, instead of saying that some of our cut-elimination proofs are 
external and that we have to resort to alien technology, we might say 
that we can duplicate the alien technology by our own, so making for 
perfectly internal proofs. The question is not whether we can `do 
it', but whether we can `do it better', given that the calculus of 
structures is more general.

Interesting paper!

Ciao,

-Alessio


At 11:01 +1000 12/9/06, Alwen Tiu wrote:
> Hi,
> Rajeev Gore and I recently wrote a paper on relating display logics
> and the calculus of structures. We did a case study on encoding
> classical modal display logic (CMDL) of Wansing into CoS.
> Through primitive extensions of CMDL, we managed to get a minimal
> cut free CoS system for S5.
> Details of the paper is given below, including a link to a draft.
> Comments and suggestions are most welcome.
>
> -Alwen
>
> --
>
> Classical Modal Display Logic in the Calculus of Structures and
> Minimal and Cut-free Deep Inference Calculi for S5
> by Rajeev Gore and Alwen Tiu.
>
> Abstract:
> We begin by showing how to faithfully encode the Classical Modal
> Display Logic (CMDL) of Wansing into the Calculus Of Structures
> (CoS) of Guglielmi.  Since every CMDL calculus enjoys
> cut-elimination, we obtain a cut-elimination theorem for all
> corresponding CoS calculi. We then show how our result leads to a
> minimal cut-free CoS calculus for modal logic $\SFive$. As far as we know,
> no other existing CoS calculi for $\SFive$ enjoy both these properties
> simultaneously.
>
> Link: http://users.rsise.anu.edu.au/~tiu/papers/cmdl.pdf