1. General
   1. Isn't the calculus of structures just a trivial notational variation of the sequent calculus?
   2. Proof theory is famous for producing horrible proofs of its own theorems; are you doing any better?
   3. What is deep inference?
   4. What is a structure?
   5. Isn't the word `structure´ reserved for semantics?
   6. Can you do in the calculus of structures anything you can do in the sequent calculus?
   7. Does the calculus of structures automatically introduce a mix rule in any system?
2. Cut Elimination
   1. You make a big deal of having the cut rule in atomic form; but can't you do the same in the sequent calculus?
   2. What's the point in proving again cut elimination for classical and linear logic?
   3. By the way, what's the point in dedicating an entire paper to such an easy statement as cut elimination for propositional classical logic in the calculus of structures?
3. Term Rewriting
   1. Isn't a system in the calculus of structures just a term rewriting system (modulo an equational theory)?
   2. If so, why not using the term rewriting terminology and conventions?
   3. But then what about rewriting logic?
4. Philosophy
   1. Do the inference rules in the calculus of structures have an associated theory of meaning, like the inference rules in the sequent calculus and natural deduction?

1General

1.1Isn't the calculus of structures just a trivial notational variation of the sequent calculus?

No, the calculus of structures uses deep inference, abolishes the distinction between formula and sequent and exploits a symmetry between premise and conclusion in inference rules: these are not features of the sequent calculus and they require new techniques.

There are other formalisms which use deep inference, but none (as far as we know) allows for the same kind of proof-theoretical analysis of the sequent calculus, for example cut elimination. The only exception is Schütte's presentation of logic, which uses deep inference, but doesn't drop the distinction between formula and sequent and does not exploit a premise-conclusion symmetry (for example, its cut rule has two premises). The proof theory of Schütte doesn't differ significantly from the usual (Gentzen) one, and does not achieve more.

One can argue that the display calculus uses a form of deep inference, but again the two other features of the calculus of structures are not exploited.

1.2Proof theory is famous for producing horrible proofs of its own theorems; are you doing any better?

Not as much as we'd like to: we have our fair share of lengthy case analyses, but luckily we can prove very elegant theorems. On the other hand, some of our proofs are very compact, much better than their counterparts in the sequent calculus, for example cut elimination and consistency for classical logic.

1.3What is deep inference?

It's deducing inside a formula, or structure, at any depth. Sequent calculus rules only see the root of formulae, what we call `shallow inference´; rules in the calculus of structures, instead, can rewrite at any position in the formula tree.

1.4What is a structure?

It's a formula modulo an equivalence relation: it can be thought of as a sequent, which usually is an expression modulo associativity, commutativity, etc. We do not call it `sequent´ because we abolish the distinction between formulae and sequents, so the structure is sort of an intermediate kind of object.

1.5Isn't the word `structure´ reserved for semantics?

This term is used in many places, but there is a tradition in philosophical proof theory which uses `structure´ the same way we do. In addition, in a certain sense, all our inference rules are `structural´ in the general proof theoretical meaning. In fact, we have no connectives: our expressions are sets plus structure, they are not very different from semantic structures in the usual sense.

1.6Can you do in the calculus of structures anything you can do in the sequent calculus?

For systems with involutive negation, yes. In this case one can trivially translate a system in the sequent calculus into an isomorphic one in the calculus of structures which has an isomorphic proof theory: it would just be a change of notation. Of course, the point is that one can do more than just this.

For systems without involutive negation, like intuitionistic logic, it is possible to use the calculus of structures in its present form by using polarities, or asymmetric logical relations like implication.

It is certainly possible to generalise the calculus of structures in such a way that it can deal trivially with any system in the sequent calculus, irrespective of negation. We don't know how many of the new properties could be retained in such a case, but we conjecture that most of them would be preserved, so this appears to be an interesting research direction for the future.

1.7Does the calculus of structures automatically introduce a mix rule in any system?

No! It happened that the first system studied in the calculus of structures (system BV) required (the analogous of) the mix rule, but that's it. All other systems do without, unless one explicitly wants (the analogous of) mix.

2Cut Elimination

2.1You make a big deal of having the cut rule in atomic form; but can't you do the same in the sequent calculus?

Of course atomic cut is sound and admissible for the sequent calculus, as a direct consequence of the cut elimination theorem. Still we make a big deal of our atomic cut, for two reasons:

First, for reducing generic cuts to atomic cuts in the sequent calculus one has to go through the cut elimination procedure, which is in general complex. On the contrary, in the calculus of structures the reduction is trivial and local (i.e., rewriting only occurs in a bounded portion of the proof). We exploit the nice consequences of this easy reduction, and in particular we prove cut elimination thanks to it, and not the other way round.

Second, in the sequent calculus the reduction of cut to atomic form only works for proofs (i.e., derivations without premises). In the calculus of structures, the reduction works in any derivation. As a consequence, we can prove decomposition theorems, i.e., statements about the constructive existence of several nice normal forms based on the partitioning of formal systems into disjoint fragments.

2.2What's the point in proving again cut elimination for classical and linear logic?

Our deductive systems are very different than those in the sequent calculus, so cut elimination is not a trivial issue. We can prove cut elimination by resorting to the sequent calculus through a translation, but we are also interested in doing so directly inside the calculus of structures. The reasons for doing so are: 1) it's very challenging, due to deep inference; 2) it opens new perspectives for computational interpretations. For example, we are able to type diagrams associated to beta reductions with sharing much better than other formalisms can do.

2.3By the way, what's the point in dedicating an entire paper to such an easy statement as cut elimination for propositional classical logic in the calculus of structures?

One of the favourite activities of mathematicians is trying to render more and more trivial the proofs of important old statements. This activity is more than just a sport, it leads to better understanding a subject and often to applications. It's also known that finding easy proofs is very difficult.

We are sorry if you feel offended by us remarking so obvious common sense facts, but we had a referee report from somebody complaining about an almost trivial cut elimination proof not being enough for a paper.

3Term Rewriting

3.1Isn't a system in the calculus of structures just a term rewriting system (modulo an equational theory)?

Essentially, yes (one has to be a bit careful and give different type to variables for atoms and variables for generic structures). Deep inference naturally corresponds to rewriting in a term rewriting system, shallow inference requires the (less natural) constraining of rewriting to the root of terms.

3.2If so, why not using the term rewriting terminology and conventions?

Because we are actually doing proof theory, and it is easier to address typical proof theoretical problems by using as close as possible a terminology to the one already in use. Moreover, in term rewriting one has to choose in which direction rewriting occurs, while derivations can be considered as growing both from top to bottom and from bottom to top.

3.3But then what about rewriting logic?

Rewriting logic also employs term rewriting modulo equational theories, but its purpose is very different from ours. Rewriting logic is an extremely general formalism, which is more about describing uniformly and implementing many different systems than performing concrete proof theoretical investigations.

4Philosophy

4.1Do the inference rules in the calculus of structures have an associated theory of meaning, like the inference rules in the sequent calculus and natural deduction?

So far, no. We have no philosophical analysis backing our investigation. But we are strongly guided by aesthetic principles: our rules are very simple and they all come from common simple schemes, irrespective of the logical systems they belong to. This cannot be a coincidence and we believe that in due time an appropriate philosophical justification will be found. For now, we content ourselves of studying the many new proof theoretical properties that are made possible by our formalism.

Back to the Calculus of Structures

15.8.2003Alessio Guglielmiemail