Subject: Re: BV on display
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-08-04 23:13:21 GMT (3 years, 47 weeks, 6 days, 6 hours and 13 minutes ago)
> At 15:31 +0200 3/8/05, Alwen Tiu wrote: > >a |- a > >------- > >a;I |- a > >-------- > >I |- *a ; a If this is not what you want then you need to use different units. Then introduce some discipline to sort out when the units should behave in certain desired ways. You are trying to do too much with just one unit. > 2) This one is quick. It seems like what DC has to offer to CoS is a > general cut elimination theorem that only requires checking some > `local' conditions on inference rules. I don't know this theorem in > sufficient detail, but, after looking at Belnap's papers, it seems > to me that the theorem works for a shallow, i.e., normal, version of > the cut rule. The theorem and the rule has to be considered in conjunction with the display property. Although it is a shallow cut rule, the display property does give us some aspects of deep inference (all aspects if you believe Jon's ranting :) > However, in CoS we have a much more general cut rule, and, in fact, > proving cut elimination in CoS is harder than in the sequent > calculus, and, most likely, in DC. This is possible but I can offer no insights. raj