Re:Calculus of structures and sequent calculus

Thanks for the comments. Let me add some... from an algebraist 
that do not understand many things about logics!

> I also find it very difficult to find inspiration in syntax, in particular in 
> that of CoS, which is still very hard for me, despite being rather familiar 
> with it. When I think about deductions, I think in terms of relation webs 
> (which is my pet semantics) or in terms of certain proof nets which I have 
> vaguely in mind.

Is it possible to have some insight on relation webs and "certain proof 
nets"?

> As a matter of fact, when I started this business, CoS was only meant to be a 
> by-product of semantics. I didn't suspect it would have had so much future 
> and most of my plans were about developing relation web semantics. I started 
> changing my mind on this only after seeing the very fast progress Alwen, Kai 
> and Lutz were doing, mostly by just manipulating syntax.

Speaking of syntax, I've find out that some people were rebuffed by the 
notations (.,.) and [.,.] for usual connectives. Why use these ones? 
Wouldn't be the systems clearer if the "old" ones were used instead?

> CoS is still young, so it can only improve in its psychological and 
> methodological helpfulness. In some cases, it's the only clean and simple way 
> of presenting certain logics, like several modal logics and systems like BV 
> and NEL, which can represent process algebras like CCS. In all these cases, 
> the sequent calculus fails so badly that CoS has clearly a psychological 
> advantage: at least you can write papers that can be read by normal people 
> and not just expert cryptographers and Egyptologists.

Errr, normal people? I'm joking, but I think CoS is much easier to read 
for mathematicians (at least algebraists).

I've been in a math lab where few people knew anything about proof theory; 
when some of them (and I was in this "some") were presented with some 
sequent calculus, they had the feeling that these objects were nearly 
algebraic (I mean they can have a generators/relations presentation). But 
only nearly algebraic: something lacked or was badly written in its 
presentation.

Then, when I first met Lutz, I had the feeling that CoS was, in some way, 
an algebraisation of sequent calculus. What I mean is: I have the feeling 
that CoS is a very good entry in proof theory for mathematicians. Some 
evolution of CoS might be even better, but it is already a much more 
mathematical object than sequent calculus (and thus I prefer CoS, 
naturally!).

> I should mention the unquestionable fact that in any case the syntax of CoS 
> is by far the cleanest available, and it's the only uniform one. *Each* of 
> the tens of systems we produced so far wins the comparison with their sequent 
> calculus counterpart in terms of elegance, conciseness, uniformity, etc. This 
> has a psychological value of some sort, because at least you work with nice 
> stuff. It might not be easy for those not used to CoS, but, as always, 
> elegance has a price. I guess it's like learning to walk on high heels, or 
> something like that.

Elegance is also a matter of personnal feeling. I've never heard any real 
argument for using a categorical language, rather than a more concrete 
one: some people like it for its elegance, some other hate it for its 
abstraction (in fact, this is also a pro argument also).

But here, there is maybe some concrete and objective way to compare CoS 
and sequent calculus. The first question I have in mind is: is there some 
kind of definition for the fact that a formal system describes proofs in 
classical/linear/intuitionistic/etc. logic?

If so, this yields a way to separate formalisms from logics. And thus to 
separate debates like CoS>sequents and linear>classical. This is of 
interest for me, since I do not understand arguments in the second one.

As I already said to Alessio, I have the analogy with universal algebra in 
mind: there are many algebraic structures (groups, rings, etc. ~ logics) 
and many objects to describe each one (operads, Lawvere theories, 
3-categories, etc. ~ formalisms).

If this analogy stands, then I can see how to compare the properties of 
two formal systems representing the same logic (like 3-categories > 
Lawvere theories for commutative structures).

But then, I don't see the point of the debate linear > classical (are 
groups better than rings?)...

> All that said, there are huge *technical* advantages in moving from the 
> sequent calculus to CoS if one is interested in certain proof-theoretic 
> objectives. These objectives are actually all the hot ones, in my opinion; 
> they are:
> 1) Getting rid of bureaucracy in proofs;

This is the one I think I understand. Since CoS admits an algebraic 
presentation (ensured by locality), bureaucracy is given by the equations 
of the algebraic structure of formulas (I'm sorry, I can't say 
"structures" for logical expressions, for obvious reasons!). The more 
algebraic structure on formulas, the more relations; and the more 
relations, the more control on bureaucracy.

This objective is the one that can deeply link proof theory with algebra. 
This is useful in both directions: algebraists can understand a bit of 
proof theory (at least!) and proof theroy can benefit from some huge 
machinery from mathematics (homotopical algebra being the most obvious for 
me).

> 2) Finding reasonable, interesting and useful semantics of proofs;

I don't really understand this one, since I've never understood what is a 
semantic (is it a map preserving some kind of structure?). But this is 
link to a question I've heard from a sequent calculus user: is there any 
semantic for CoS, really different from proofs? (I do not get the point 
here, maybe you can help me).

> One of my personal research objectives is to get to a formalism which I'm 
> calling at present `deductive derivation nets'. I can't tell you much about 
> the categories it lives in, and I don't think the algebraic topology needed 
> to classify its proofs exists already. However, I can right now draw on the 
> blackboard its proofs, and everybody would agree with me that they are 
> deductive, there is no bureaucracy, and you can state and solve problems like 
> identity of proofs therein.

This is really interesting to me. Maybe we can discuss it next week, since 
I have some vague intuitions on what kind of algebraic topology would be 
involved.

> I hope I didn't forget anything. I should say that I wrote this very hastily 
> (I'm much pressed for time, these days). Please send me comments and 
> suggestions. Maybe we can turn this text into something to be put on one of 
> our web pages?

Thanks for taking some time to write it. Maybe some kind of >> objective << 
comparison could be written between the two formalisms. Stating all the 
known properties of each formalism for any logic, together with the links 
between them, might be a good way to convince sequent calculus addicts to 
(at least) take a look to CoS.

> Anyway, conclusion: my (certainly very biased and immodest) opinion on CoS vs 
> sequent calculus is the following. I don't see CoS taking the place of the 
> sequent calculus in elementary textbooks. However, I do think that CoS and 
> deep inference will be more and more central to the development of 
> (structural) proof theory in the next ten years, and I think they will become 
> part of the classical landscape in the discipline very soon.

I hope so!

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.

Thanks again in advance for any comment,

yves