Substructurally Yours

There has been a lot of interesting work on substructural logics coming out of Japan for a while now. The class of logics which has received the most attention are the so-called FL logics. FL stands for Full Lambek Calculus and is what you get if you drop the structural rules of weakening, exchange and contraction from intuitionistic logic. If you prefer other terminology, this is the same as noncommutative multiplicative additive linear logic.

What makes FL particularly nice is that it has a perspicuous algebraic semantics given by residuated lattices. Briefly, a residuated lattice is a set that carries both a monoid and a lattice structure such that the monoid has both right and left residuals. These may be seen as left and right division operators and satisfy the properties that x.y &le z iff x &le z/y iff y &le x\z. Categorically, this corresponds to saying that we have a biclosed monoidal category with both finite sums and finite products. A residuated lattice is the special case where the category is a poset.

Given FL as a base, we can build up other substructural logics by adding structural rules. These may be the standard weakening, contraction and exchange rules or more exotic rules with cute names like mingle and expansion.

So, what counts as a structural rule? And in what way does the property of an extension of FL rely on the structure of the additional structural rules? These questions and much more are answered in the following paper:

Which Structural Rules Admit Cut Elimination? - An Algebraic Criterion. Kazushige Terui

This paper is chock full of interesting stuff, so I will only sketch bits of it. In order to keep you reading, I'll state one of the main results in grandiose wording. Every substructural logic over FL has cut elimination! Wowzer!

Let's try make this a bit more precise. First, an example. Say we take FL and add contraction but not exchange. Then, the resulting calculus is quite easily seen to not have cut elimination. So the grandiose statement needs some refinement. Specifically, if we identify a logic with its set of provable formulae/sequents, then the result says that any such logic over FL can be given a cut free sequent calculus. Still cool.

How does this all work? It pushes through in a way that is very familiar from exotic structural proof theory, such as the calculus of structures. First, say that a structural rule satisfies the syntactic propagation property if it propagates from atomic formulae to all formulae. In other words, all instances of the rule can be reduced to atomic instances.

Returning to our example of FL with contraction but no exchange, let's extend contraction to act on arbitrary sequences of formulae. Then, this modified version satisfies the syntactic propagation property, while the version with standard exchange does not. We may be onto something here!

As it so happens, Terui shows that every extension of FL having cut elimination satisfies the syntactic propagation property on all of its structural rules. What about the converse? It turns out that this is true also, but in order to prove it, Terui introduces a semantic propagation property. This property is stated in terms of, you guessed it, fancy sorts of residuated lattices.

So, a structural extension of FL has cut elimination iff it satisfies the syntactic propagation property iff it satisfies the semantic propagation property. Our tweaked version of FL with contraction satisfies syntactic propagation, so has cut elimination. This is a special case of a more general phenomenon. Given any collection of structural rules, we can complete them (in the Knuth-Bendix sense) to another set of structural rules that results in cut elimination. Moreover, this completion preserves provability. Now that is super cool!

Anyway, I'll stop there and point you to the paper for lots more juicy details!

On a side note, I am in Perth now for the Australasian Association of Logic annual conference, as well as the Australian Mathematical Society annual conference (since the movie was boring, I read the above paper and wrote this post on the plane flight over). The latter has streams in logic and algebra, which I will generally be hanging around. I'll even be giving talks in each conference (the things they let me get away with!). I'll be blogging details as the conferences progress. Whether this will be liveblogging depends on whether I can leech some wireless. Otherwise, I'll try to do daily posts.