Re: Calculus of structures and sequent calculus

Dear Yves,

> By the way, I have another question. What can be said about cut 
> elimination in CoS (in the absolute, but also with respect to the one 
> of sequent calculus)? I kind of like the way it is described in CoS (I 
> mean as a factorisation of derivations, if I get the idea) and would 
> like to know if it's possible to express it as a local computation on 
> derivations.
>
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 I find more exciting is the following. There are these 
factorisations of derivations that you mention in Lutz's and in my 
thesis, and they entail cut elimination. My favourite one is what we 
call interpolation: it's the symmetric closure of cut elimination. This 
is strictly stronger than cut elimination in the sequent calculus, 
unthinkable in the sequent calculus, and, as Richard observed, actually 
is telling us something new about Craig's interpolation theorem. But 
most importantly it's beautiful! There is a proof of it for 
propositional logic in my thesis that uses semantics and thus doesn't 
scale to predicate logic. I'm working on a funny syntactic proof.

I don't know about locality of cut elimination. It depends on you notion 
of locality. Do you have an example of cut elimination procedures in the 
sequent calculus that you consider local? We have Tait-style (in some 
sense global) and Gentzen-style (in some sense local) proof 
transformations for eliminating the cut. Personally, I consider both of 
them non-local since also Gentzen's procedure is duplicating 
unbounded-size trees all over. If your notion of locality is as strict 
as mine, then I think we don't have a local cut elimination procedure 
and I wonder whether there is one at all.

Btw, Tait-style is more natural for classical logic in CoS, because in 
doing it Gentzen-style most of the local proof transformations simply 
don't do anything (think atomic cut). It's trivially possible to do it 
Gentzen-style, but we learn nothing from that.

I'll see you in Dresden so we can chat there. Btw, I tried to read the 
introduction of your thesis. I was impressed but had to give up in the 
end. Can you recommend an introductory exposition of higher-dimensional 
rewriting which is written in English?

-Kai