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
