A little while ago, I was chatting with an algebraist and he asked whether I knew of any invariants for logics. Now, when a mathematician asks for an invariant, he is asking for something rather particular. This is best explained through some examples.
The simplest example of an invariant is this. Let F be the collection of all finite sets. Then, we can define an invariant function, c, which maps F to the natural numbers and takes a finite set to its cardinality. What is this an invariant of? Well, it is an invariant of the "equivalence" class of a finite set. That is, if two finite sets have different cardinality, then they cannot be isomorphic. Actually, in the case of finite sets, this invariant is complete, in the sense that two finite sets are isomorphic if and only if they have the same cardinality.
A more substantial example is given by the fundamental group of a topological space or, more generally, the sequence of homotopy groups. These do not always characterise the space as tightly as cardinalities do for finite sets, but Whitehead's Theorem
says that it characterises homotopy equivalence if the space is sufficiently nice.Edit:
This is not quite correct, see the comments.
So, let's get back to logic. What sorts of invariants could we hope for here? One option is to just say that the algebraic models are invariants of the logic. For instance, propositional logic is essentially the theory of boolean algebras, intuitionistic logic of Heyting algebras and so on. Alternatively, we could grab some categorical models as invariants. So, for linear logic we get star-autonomous categories, for intuitionistic logic we get cartesian closed categories and so on.
Using algebraic or categorical models as invariants for logics is highly undesirable. This is because an invariant should be a simpler
than the gadget it is an invariant of. Algebraic and/or categorical models are more like mirror images of the logic under consideration.
It turns out, that if we use some trickery, we can actually make some progress. Suppose that we have a set with an associative binary operator. Now, in virtue of having a binary operator, we can view the terms of this algebra as binary trees. The associativity criterion then becomes a criterion for identifying trees. Now, let's think about automorphisms of this space. Any automorphism, mapping trees to trees, must map trees of the same length to trees of the same length. Moreover, any two trees of the same length are "isomorphic", so permuting them is an automorphism. Now, if we think of the permutations as being composed of our basic associativity map a(bc) -> (ab)c, then we can ask to ensure that any two sequences of applications of this rule which result in this permutation should be identified. If you know anything about categorical coherence theory, you should be jumping up and down and waving Mac Lane's pentagon under my nose right about now. Indeed, the classical coherence theorem for monoidal categories can be used here. Used for what? Well, for helping to write down a collection of generators and relations for the automorphism group, of course!
When the dust has settled and we look at what the automorphism group is, it turns out to be very famous indeed. It is a group known as "Thompson's Group F
", which has been the object of much study over the past forty years or so.
So, we can say that an invariant of the logic consisting of only an associative conjunction (not necessarily commutative) is Thomson's F. Using simlar trickery, we can discover that making the conjunction commutative also, results in Thomson's Group V. A very nice paper discussing all of this (with no mention of logic, mind you) is:Geometric presentations for Thompson's groups
; Patrick Dehornoy
Being able to calculate what Dehornoy calls "geometric groups" for algebraic identities paves the way for calculating invariants of logics. Certainly, we are still rather far from invariants of a reasonable complex logic, but this could well be the starting point for a fascinating link between substructural logic and algebra. If you are interested in this and wish to pursue it further, then please get in touch with me!