That Logic Blog

March 07, 2006

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 p1,...,pn, then we also have f(p1,...,pn).

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 Xn, for some object X where, as usual, Xn is defined to be X x Xn-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 GT:2-Fin → T, such that GT 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.

8 Comments:

Blogger Kenny said...

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".

Is this really a different notion? My understanding of some simple stuff that algebraic geometers do is that they take some ring R, form Spec(R) - the set of all maximal (or is it prime?) ideals in this ring, with the basic closed sets given as the collections of maximal ideals extending any given ideal. A variety is just a closed subset of Spec(R).

One example of this is to let the ring R be a boolean algebra - in particular, let's take the Lindenbaum algebra in some language! Then a maximal/prime ideal is the set of negations of formulas in some maximal consistent set, so we can identify each point of Spec(R) with a class of elementarily equivalent structures. If we have some consistent set T of formulas (our theory), then their negations generate an ideal. The closed set corresponding to this ideal contains all structures satisfying T. Thus, sets of structures satisfying a theory exactly correspond to closed sets (varieties) in the Lindenbaum algebra.

I remember hearing about this "H/S/P" thing when I first learned about algebraic logic, but I'm not sure how that might relate. I suppose that was before I took algebraic geometry, but this correspondence is why I figured they both used the term "variety", even though the uses are different on the surface.

3:53 PM  
Anonymous Jon said...

Neat observation! I think that the major difference is that you have an equationally defined collection of elements in a particular boolean algebra, whereas a universal algebraic variety studies the (equationally defined) collection of all boolean algebras.

The construction you outline strikes me as being very similar to the one used in the Stone representation theorem (basic open sets are the collections of all principal ultrafilters on some element of the boolean algebra).

The universal algebra definition certainly came later. I guess the thought process was something like "these algebraic geometers are studying the sets of solutions of a collection of (polynomial) equations. Hey, we're studying the "sets" of solutions of a collection of equations. Let's call it a variety too, in order to confuse anyone who uses the term!".

9:45 PM  
Blogger Kenny said...

The Stone representation theorem is what made me notice this connection, because I saw it at about the same time as I saw the Zariski topology in my algebraic geometry class, and I noticed these are exactly the same thing.

As for the distinction between a variety in a boolean algebra, and the variety of all boolean algebras, I don't think that's terribly significant. After all, this latter variety is just a variety in the former sense within the single boolean algebra given by the first-order language with two binary operations, a unary operation, and two constants.

Of course, the analogy works on the syntactic side, where you consider the boolean algebra of sentences, and universal algebraists are looking on the semantic side, where we consider the class of all structures satisfying the formulas. In algebraic geometry, this corresponds to looking at it geometrically rather than algebraically, except with the individual points replaced by proper classes of models.

8:23 PM  
Anonymous Anonymous said...

link to catsurv.ps paper nonfunctional, but this works (for me)

aix1.uottawa.ca/~rblute/catsurv.ps

4:25 PM  
Blogger John Baez said...

Wow, this stuff you're talking about is great!

You write:

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.

I was pondering this when writing "week227" of This Week's Finds. It seems a real pity that the "categories as theories" over in abstract algebraic logic don't seem to be talking to the "categories with proofs as morphisms" over in proof theory.

I can't believe this is an inherent defect! I feel that either I don't know what the really cool people do to connect these subjects... or they haven't started connecting them yet.

Certainly given a so-called sketch of an algebraic theory, I can make up a precise notion of a proof that two morphisms in the resulting category with finite products are equal. We do, after all, use sketches to prove such things!

But I guess this gets us into the realm of 2-theories, since now we're not just talking about morphisms in a category with finite products being equal or not: we're talking about proofs that they're equal, which we should think of as 2-isomorphisms.

Hmm, I just now noticed that your post was on 2-theories. So was the stuff I'm saying now actually part of your point? :-)

Maybe I'm just catching up with you.

9:03 AM  
Anonymous Jon said...

Anon: Thanks, I have fixed the link.

Kenny: I suppose the distinction is not terribly significant, but it was all that I could think of :-)

John: Yes, what you are saying is part of my point. I think that an adequate "2-theory" is going to need to deal with contravariance. Perhaps we need to focus on algebras for 2-monads on the 2-category of representable polycategories?

9:34 PM  
Blogger youluvkaila said...

i think that you need to keep your postings short and sweet. they are too long. I am not trying to sound mean because u r a great writer, just make them short!!!!

3:14 AM  
Anonymous Anonymous said...

Hello. Enjoyed your blog. I like the design and you have great content. Keep up the good work.

To see reviews of the Top Dating Sites please visit this site.

4:18 AM  

Post a Comment

<< Home