Friday, March 09, 2007

Fixed point logics

At CUSPOMMS today, the audience was depressingly tiny, which was a great shame because Anuj Dawar gave a terrific introductory talk about the problems he is working on in finite model theory. In a particular, he said a little about the expressive power of logics which have a 'least fixed point' operator, and the relation of this to the question whether P = NP.

The topic of fixed point logics links up very closely with something I need to think about soon, for I've promised to put together a talk on Dan Isaacson's Conjecture for a workshop next month (I mean the claim that, if we are to give a rationally compelling proof of any true sentence of the language of first-order arithmetic which is independent of PA, then we will need to appeal to ideas that go beyond those which are constitutive of our understanding of basic arithmetic). What's the connection? Well, it is plausible that our understanding of arithmetic involves grasp of the ancestral of the successor relation ("the natural numbers are 0, the next number, the next one, the one after that, and so on, and nothing else"). So it is natural to think about theories of arithmetic which are embedded in stronger-then-first-order logics with a primitive ancestral-forming operator (i.e. a transitive closure operator, which is closely related to a least fixed point operator). We know that such arithmetics semantically entail more than PA but are unaxiomatizable. But what about partial axiomatizations of them? I know that the very natural partial axiomatization that goes back to Myhill gives us a theory which is in fact a conservative extension of PA (so that result is in harmony with Isaacson's Conjecture: trying to pin down a concept arguably essential to our understanding of arithmetic which isn't definable in the language of PA still doesn't take us beyond PA). But I need to discover more about fixed point logics to see what else interesting is to be said here.

Anuj recommended Leonid Libkin's Elements of Finite Model Theory as a good place to start finding out more. Great. I've ordered a copy.

Back to category theory

Back in August, I did a bit of reading on category theory. I'm now taking that up again with a group of graduate students. We've started working through Robert Goldblatt's Topoi: The Categorical Analysis of Logic (an amazing bargain reprint from Dover). And this time I'm getting more of a feel for what is going on. Or at least, I have the comforting illusion of understanding -- but it could all be shattered soon, when it is my turn to talk at the reading group next week, supposedly helping us through chapters 5 and 6.

Up to about half-way through chapter 3, Goldblatt proceeds at a pretty gentle pace; he then accelerates a bit alarmingly. Reading his first three chapters in parallel with the first six chapters of Steve Awodey's Category Theory works well, however, if you have the time.

And is the effort worth it? Well, we'll see (though my sense so far is that the answer should be very positive). But in the meantime, we're certainly having fun ...