That Logic Blog

January 10, 2006

Invariants

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!

6 Comments:

Blogger David R. MacIver said...

I think your characterisation of Whitehead's theorem is wrong. My impression (but this is based on admittedly vague memories) is that you cannot strengthen it to say that CW-complexes with the same homotopy groups are homotopy equivalent - you really do need to assume that the map which induces the isomorphism between all the homotopy groups exists. Thus the homotopy groups don't actually provide a complete set of invariants for CW-complexs mod homotopy.

I can't remember what the examples that proved this were though.

4:06 AM  
Anonymous Anonymous said...

Thanks for the clarification David. I'll have to be more careful when drawing wild analogies with topology in future :-) On the other hand, a counterexample would be interesting to see - I'll have to have a dig around for one.

9:37 AM  
Blogger John Baez said...

Yeah, Whitehead's theorem says that if a
map between CW complexes induces an isomorphism on homotopy groups, it's a homotopy equivalence. But two CW complexes can have the same homotopy groups without being homotopy equivalent.

The point is, the homotopy groups "talk to each other" in complicated and interesting ways.

The first place you see this is when you have a space with two nontrivial homotopy groups - if there's just one nontrivial homotopy group, that really does completely classify your space.

So, suppose you have a connected CW complex with only pi_1 and pi_2 being nontrivial. This is called a "connected homotopy 2-type". It turns out that to classify such spaces, you need a bit more information than these two groups: you also need an action of pi_1 on pi_2, as well as a 3-cocycle, which is a map

f: pi_1 x pi_1 x pi_1 -> pi_2

satisfying the big equation on page 59
in this paper of mine.

The 3-cocycle business is a bit scary unless you like monoidal categories and realize that the 3-cocycle equation is just the pentagon identity in disguise... I explain this in that paper.

But never mind: you can always take the 3-cocycle to be trivial (just zero), and then you only have the action of pi_1 on pi_2 to contend with. And this is quite easy to comprehend: an element of pi_2 looks like a balloon, while an element of pi_1 looks like a loop of string... and you can stretch a balloon around a loop of string to get a new balloon!

So, you can build two really different spaces both with pi_1 = Z/2, pi_2 = Z, both with trivial 3-cocycles, but with different actions of pi_1 on pi_2.

In the first, let pi_1 act on pi_2 trivially. This space is just

RP^infinity x CP^infinity

since the infinite-dimensional real projective space RP^infinity is the space with pi_1 = Z/2, while the complex one CP^infinity is the space with pi_2 = Z - with all other homotopy groups vanishing in each case.

In the second, let pi_1 = Z/2 act on pi_2 = Z nontrivially, by negation. Then we get a nontrivial CP^infinity bundle over RP^infinity, vaguely like a heavy-duty Mobius strip, where the CP^infinity reverses orientation as you carry it around any noncontractible loop in RP^infinity.

Wow, it was fun figuring out that concrete example... hope it wasn't too boring.

Anyway, the real cool thing is that homotopy n-types are secretly n-groupoids - special sorts of n-categories - and there's a lot more information in those than merely a list of n groups.

Right now I'm in Marseille at a workshop on the geometry of computation where logic and computer science people are talking to category and topology people like me... and this stuff is exactly the kind of thing we're talking about: topological invariants of logical systems!

And sitting in the library a few minutes ago, I saw a cool paper on cohomology of Lawvere theories... same stuff.

10:17 PM  
Blogger John Baez said...

Here's that paper on cohomology for Lawvere theories, in case your algebraist friend is interested:

Mamuka Jibladze and Teimuraz Pirashvili, Quillen cohomology and Baues-Wirsching cohomology for algebraic theories, Max-Planck Institute fuer Mathematik Preprint Series 2005 (86).

They show that three approaches to defining the cohomology of a Lawvere theory agree. The way that I like - the Quillen way - uses the bar construction.

Alas, I don't see any explicit calculations for examples!

10:58 PM  
Anonymous Anonymous said...

Hi John: Thanks very much for the explanation and the links! I'll certainly have a read through of the notes from your course once I settle in properly here.

10:17 PM  
Anonymous Anonymous said...

If you want a category theoretic take on Thompson's group F see 'A simple description of Thompson's group F' by Marcelo Fiore & Tom Leinster here.

6:26 AM  

Post a Comment

<< Home