Subject: Re:Paper announcement: CMDL in CoS
Newsgroups: gmane.science.mathematics.frogs
Date: 2006-09-16 13:04:52 GMT (1 year, 33 weeks, 5 days and 28 minutes ago)
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