Re: Calculus of structures and 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.

Yes. What I meant is that *once you know what to do*, you have to
struggle just a bit in order to make cut elimination work for
predicate logic in CoS. For propositional logic, which you probably
have in mind, there is no struggle at all, in fact it's much easier
than in the sequent calculus -- again, once you know what to do.

-Kai