2-Theories

Let's return to the question of what a logic is. This time, we'll leave philosophical concerns at the door and approach the question like a mathematician. Ahem.

Any logic you come across in the wild is going to have the same basic structure. It will have a set of "atomic" variables, A, and some operations that can be applied to this set. These include things like conjunction and negation, as well as scarier things like quantifiers. For today, let's pretend that quantifiers don't exist. Then, a logic is the "free structure generated by the given operations over A". For instance, say we have an n-ary connective, f. Then, whenever we have n things in our logic, say p₁,...,p_n, then we also have f(p₁,...,p_n).

Well, this still feels a bit wishy-washy. Can we be more mathematically precise? Yes we can. One classical way is to construct the Lindenbaum-Tarski algebra of the logic. The idea behind this construction is to pretend that the logical operations are algebraic operations and squint until you get a universal algebra (more technically, quotient out by the evident equivalence relation generated by implication).

Very well. So, we have a first pass at defining a logic: it is a "free universal algebra". All this means is that we grab some set A and some equational theory E and study the properties that any object satisfying E must satisfy (with the variables drawn from A, but this doesn't really matter). A theorem due to Birkhoff says that this is the same as a variety. Now, "variety" in this sense means a class of algebraic structures closed under homomorphic images, subalgebras and products. This is a different notion from what algebraic geometers mean by "variety". Examples of varieties are groups, rings, lattices,... So, studying a particular logic is "the same" as studying the variety of algebras that satisfy the equational theory of the logic (well, sometimes you have to consider universal Horn clauses, in which case you study "quasivarieties"). This is the classical point of view of algebraic logic. A cool introduction to this sort of thing is:

A Survey of Abstract Algebraic Logic; J. M. Font , R. Jansana and D. Pigozzi

If you don't have a subscription to Studia Logica, you can check out Chapter II of:

Algebraic logic; Hajnal Andréka, István Németi and Ildikó Sain

Abstract algebraic logic is a good start to understanding what logic is from a mathematical point of view. However, it suffers from one serious objection: it does not model proofs in a logic. That is, it equates any two proofs of a given statement. This is A Bad Thing.

Happily, there is a well-defined way of modelling proofs in some "universal algebra", dating back to Lambek. It can be viewed as pushing the Lindenbaum-Tarski construction up by one dimension: instead of taking the free term algebra of the logic, take the free category of the deductive system. This is a bit of a floppy definition, but you can see more of what I mean by this in:

Category theory for linear logicians; R. Blute, P. Scott

So, we can now do one better and say that logic is the study of "free categories with structure". Examples are, of course, cartesian closed categories, which are "the same" as intuitionistic logic and star-autonomous categories, which are "the same" as multiplicative linear logic (without exponentials). Now, above I was a bit sloppy with throwing around the term "algebra". What I meant before was algebra in the sense of "variety generated by an equational theory". This is not the same thing as the more familiar meaning of alebra as "algebra over a commutative ring k", which is a ring A equipped with a ring homomorphism from k into the centre of A. The viewpoint of category theory allows us to study logic in terms of "algebra" in this sense, via so-called full completeness theorems. For instance, various flavours of Hopf algebras form models of various flavours of (multiplicative) linear logic. This is cool!

We now know that in order to find a uniform description of logics, we need a uniform description of "categories with structure". There are various ways of accomplishing this, but none that are completely satisfactory! I'll talk about other approaches in later posts, but for now let's focus on things called 2-Theories.

Algebraic theories were introduced by Lawvere, in order to study the notion of "set with structure", such as groups, rings,... Formally, an algebraic theory is a category, C with products in which each object is a finite product of some object x. We then slap some extra arrows onto this category, expressing algebraic relations. A "model" of a theory is a functor F:C → Set. John Baez has a better description of these gizmos over at:

This weeks finds in mathematical physics: week 136; John Baez

Ok, so via these whacky gadgets, we can talk about a set with added structure. Heck, we can talk about other mathematical objects with structure. For instance, there is some theory of groups, say G:C → Set. We get the theory of toppological groups by changing Set to the category of topological spaces. That is, the theory of topological groups is something like G:C → Top. So, an algebraic theory is a product-preserving functor from C to some category.

Hmmm. Can we categorify this in order to describe categories with extra structure? Well, let's see. Our category C is basically the collection of objects of the form Xⁿ, for some object X where, as usual, Xⁿ is defined to be X x X^n-1. Let's start from changing from products to coproducts. Now, any such category is basically the same as "the skeletal category of finite sets". This is just the category whose objects are the finite ordinals 1,2,... The coproduct structure is given by disjoint union. In this way, we see that every object is generated by 1 and the coproduct. Let's call this category Fin.

Now, in order to describe a "categorical theory", what we want to do is take a functor from Fin to some 2-category equipped with coproducts, which preserves coproducts. This is the same thing as a category, except we now have 2-arrows, which go between arrows. The canonical example of a 2-category is Cat, the category of all small categories. The objects are categories, the arrows are functors and the 2-arrows are natural transformations.

We're not quite done, since Fin is a 1-category and we are trying to send it to a 2-category! No problem, we can turn Fin into a 2-category by adding in all the identity 2-arrows. Let's call this 2-category 2-Fin. We can now define a 2-theory! It is a a 2-category, T, with a specified coproduct structure, together with a 2-functor G_T:2-Fin → T, such that G_T is bijective on objects and preserves the coproduct structure.

2-Theories were defined and studied in the following nifty paper:

The syntax of coherence; Noson Yanofsky.

I said before that every approach to describing categories with structure has some catch. What's the catch here? Well, you cannot use these things to model contravariant structure on a category! This is a serious concern for logicians, since, for instance, this means that it fails to capture logics with some sort of implication (which corresponds to the Hom bifunctor). Bummer.

That's enough for today. In a later post, I'll describe another approach that uses a generalisation of operads in order to get around this problem.