News

I realise that I have been a bit slack with posting recently. Apart from busily writing some papers and doing a little logic, I have been partaking in some holidaying. It's a hard life, I know.

I have also been organising the practicalities of my impending move to Sydney. From next week Monday, I shall be at The Centre of Australian Category Theory for a few months. Officially I am visiting Mike Johnson, but with the number of cool seminars within ambling distance, I will probably end up spreading myself around.

I would like to start up some NotYASS sessions in Sydney if there is sufficient interest. If you are in the area and are interested in having some drinks and partaking in a wilful disregard of academic subject boundaries, give me a holler.

Also for those in the Sydney area, I shall be participating in a weekly advanced modal logic reading group, with a bunch of people in Canberra. Naturally, I would like to have some people around to chat about this stuff in person, so if you are in the area, have some background in logic and would like to get together weekly to discuss some of the finer technical points of modal logic, let me know. We are most likely going to be using pieces of these three books, as well as selected research papers.

Some recent(ish) news from Canberra is that our logic group has continued to grow with Peter Baumgartner and Alwen Tiu both arriving over the last couple of months. Fellow student Rowan Martin-Hughes has also started up a blog, containing his musings on game theory, multi-agent systems and other such goodies. If you are interested in such things, then head on over Towards an Agent Society.

Anyway, regular posting will resume in a week or so, once I am settled in.

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!

Basic Logic

One of the common features of many philosophies of mathematics such as platonism, formalism, fictionalism and so on, is that they view mathematics as a constant, static entity. From this perspective, it makes sense claim something along the lines of "X is the correct foundation for mathematics", where X may be ZF set theory, category theory, constructive type theory or what have you.

However, a subject such as mathematics is constantly changing. So, why not allow this natural evolutionary process into your foundational doctrine? This is the view argued in a very entertaining fashion in:

Steps toward a dynamic constructivism; Giovanni Sambin.

Now, if one accepts that the body of mathematics is constantly changing and, a fortiori, that a foundational theory ought to be malleable, then the concept of mathematical truth is no longer static. This pluralist attitude towards mathematical truth may be refined to a pluralist attitude towards logic. Indeed, Sambin argues:

It is difficult to accept a plurality of logics and still believes that logic deals with a static, a priori, and hence univocal notion of truth.

Given that one accepts a pluralist position, one may seek a way in which to systematically organise various logical theories. To this end, Sambin seeks a common core for a multitude of logics, arriving at a system he calls Basic Logic, which is "the minimal core, with no structural rules". Thus, Sambin adopts a view common amongst substructural logicians of various pursuasions, though he argues via a different route. In order to understand a bit more about what Basic Logic is all about, one must turn to:

Basic logic: reflection, symmetry, visibility; Giovanni Sambin, Giulia Battilotti, Claudia Faggian.

Skipping out the ideological motivations, which are explained in the paper and implemented via a notion of "reflection", one may describe Basic Logic as being almost the logic that results from dropping weakening and contraction from intuitionistic logic. There is one additional ingredient and one technical modification. The extra ingredient is a coimplication, which is the residual or adjoint of multiplicative disjunction in exactly the same way as standard implication is the residual or adjoint of multiplicative conjunction. The technical modification is the one suppresses contexts.

While several logical systems can be seen as extensions of Basic Logic, one ought not see Basic Logic as being the ultimate core of logic and, indeed, Sambin does not claim it to be. For instance, it is an overarching assumption throughout the development that both conjunction and disjunction are commutative (so the statement that it is free of structural rules is not quite true). This is a rather strong requirement and immediately discards many interesting and useful noncommutative logics arising in linguistics and computer science.