Re: Calculus of structures and sequent calculus

At 17:13 +0100 14.2.05, Kai Brünnler wrote:
>Cut elimination procedures for the classical 
>sequent calculus roughly also work in CoS. One 
>has to struggle a bit with the greater 
>applicability of inference rules, e.g. a cut 
>does not automatically split the proof when 
>going up, and one is rewarded a bit, e.g. by 
>obtaining tight bounds for cut elimination more 
>easily than in the sequent calculus.

What is your idea of `bit'? I remember we've been 
fairly lost for many months in trying to do cut 
elimination in CoS, the reason being the loss of 
the root connective information that the sequent 
calculus has.

I think cut elimination came with *great* effort, 
and also the rewards are great (your proof for 
classical logic being a prime example of that).

To all those who wrote me: I'm a few weeks behind 
with email, but in the end I'll answer everybody 
(this comment was easy, so I did it straight 
away).

-Alessio