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.


Shawn said...

This question might be a bit basic, but could you explain what an ancestral is? Googling turns up nothing of relevance, since the cognate 'ancestor' turns up too many genealogy sites. Thanks.

Peter Smith said...

The ancestral R* of the relation R is that relation that stands to R as ancestor of stands to parent of. So R*ak is true just if there is a (finite) chain a, b, c, ..., j, k such that Rab, Rbc, Rcd, ..., Rjk.