Doing it Deeply

One of the salient features of logical formalisms such as sequent calculi, tableaux and natural deduction is that the logical inference rules attack the main connective of a formula, either introducing it or eliminating it. This is to be contrasted with the situation in, say, elementary algebra where one may apply properties such as associativity and commutativity anywhere within a formula.

One may wish to add the ability for rules to act arbitrarily deeply within a formula to a logical formalism. But how can one do this in a sensible way? For many, the most obvious reply would be to utilise term rewriting. This consists of a bunch of "rewrite rules" which allow one to rewrite one term to another anywhere deep within a structure. For example, in a transformational grammar, one may have a rule such as VP --> V + NP, which rewrites a verb phrase into a verb followed by a noun phrase (that is, into a transitive verb).

The problem with just using term rewriting is that there does not, initially, seem to be a good notion of analytic proof, which is provided in the sequent calculus by cut elimination and in natural deduction by normalisation. This is a big concern, since it is analyticity that leads to important metalogical results such as consistency, interpolation and so on. One solution that has been pioneered recently goes under the name of Calculus of Structures. A good introduction to this formalism is provided by the following two papers:

A System of Interaction and Structure, Alessio Guglielmi

Deep Inference and Symmetry in Classical Proofs, Kai Brünnler

By massaging a one sided sequent calculus via the addition of the ability for rules to act arbitrarily deeply (effectively turning them into rewrite rules), one gains the ability to act arbitrarily deeply, while clinging to some notion of analyticity. This is evidenced by the fact that one can still prove all of the same metalogical results.

While this seems promising, to date the Calculus of Structures has only been convincingly adapted to logics which have an involutive negation. In other words, anything with an intuitionistic flavour has been more or less left out in the cold (though there are current efforts to rectify this situation). Moreover, many of the broad concepts are subsumed by categorical logic, while missing out on the important categorical notion of coherence, as is pointed out in the following paper:

Deep inference proof theory equals categorical proof theory minus coherence, Dominic Hughes

Does the above paper sound the death knell for the Calculus of Structures? Probably not, though it does suggest that one needs to understand categorical proof theory when attempting to build a system with deep inference. If not, then one faces the problem of not knowing whether something is just reinventing the wheel. If so, then fitting one's formalism within the context of existing work on things such as categorical logic leads to a clearer understanding of the contribution of the work and also makes the job of selling it to people in adjoining research areas that much easier.