Sunday 15 March 2009

Testing Emacs mode for blogging

A quick google revealed that there are indeed Emacs lisp hacks that allow one to write blog posts in the comfort of all things Emacsy.

One of them, which I'm currently testing, is available at http://code.google.com/p/e-blog/. We'll see if this gets posted, and how the formatting turns out. A quick look at the Emacs lisp code suggests that while this text is auto-filled as I write it, e-blog will reformat it before submitting it to blogger.com. Well, as said, we'll see.

UPDATE: The post got happily through, as you can see. The lisp code seems to be working just fine for posting -- I'm now testing whether updating existing posts works -- and a one-line insertion to e-blog.el gave me ispell based on-the-fly spell-checking (i.e. I enabled the flyspell-mode minor mode as default for the blog posting mode). Wonderful. No longer must I suffer the horrible Google interface. One less reason to ever leave Emacs.

Pohlers versus Girard

I recently received my copy of Pohlers' Proof Theory: The First Step into Impredicativity from Amazon. Alas, I can only second Peter Smith's complaint, that the book is not particularly well written. It's stated in the back of the book Pohlers' intent was to "write a book on proof theory that needs no previous knowledge of proof theory". If so, the book quite falls short of its stated goal. It is at the same time too abstract, and too involved with irrelevant formal details, to be really approachable to those who have not yet been exposed to proof theory. This said, there's much good in the book. The systematic use of Tait-calculi in particular is something to be applauded. One finds in this book also the "quantitative" side to the Schütte-Feferman analysis of predicative explained in detail. (For the "qualitative" side Torkel's Inexhaustibility is much to be preferred -- indeed, reading Pohlers' book one will certainly learn the ordinal bounds, but quite why they should count as an analysis of predicativity in particular and not just these or those random formal theories is left almost unexplained.) Those into technical proof theory will welcome too the systematic sustained exposition of operator controlled derivations, the application of "impredicative" techniques to predicative theories, etc.

I wouldn't recommend Pohlers' text as the first introduction to proof theory. But then, I wouldn't recommend any existing text as a first introduction to proof theory. Proof theory is, it seems, an inherently messy subject, requiring bits and pieces from recursion theory, model theory, general set theory, the theory of the constructible hierarchy, descriptive set theory, and so on. Not necessarily the most profound bits, but bits nevertheless. It is possibly this dependence on in themselves rather technical fields that renders proof theory more difficult for elementary introductory expositions. (Concepts and results are necessarily pulled out of a hat, so to speak.) Nevertheless, if I absolutely had to pick a text, it would be Girard's Proof Theory and Logical Complexity. It is not that the text is necessarily any more forgiving than Pohlers', but rather that Girard is quite forthright about the tedious formalities -- and indeed explains in banal terms the point to these and those formalities, and why they're relevant or irrelevant, as the case may be, for this or that purpose -- and does not indulge in gratuitous abstraction. Experience teaches that in proof theory it is necessary to get one's hands dirty at some point. (After which one may prudently refrain from touching an actual formal proof unless absolutely necessary.) So be it. Experience also teaches that in proof theory only certain kinds of abstractions actually pay off, perhaps because we haven't found the right kind of general abstractions yet. I believe Girard manages to strike an agreeable compromise between concreteness and abstraction -- it's an empirical observation that in proof theory we raise the level of generality not by introducing abstractions and precise definitions, but rather by developing a sense of when the formal details are relevant and when they're just irrelevant fluff that can be safely ignored. Going through Girard's text one will certainly develop the relevant kind of intuition for these things. Not so with Pohlers'.

Pohlers' philosophical and historical interludes are rather telegraphic and sometimes peculiar. In contrast, while Girard too professes but the working logicians knowledge of history, his discussion of Hilbert's programme, the classification problem, the (ab)use of the incompleteness theorems by non-mathematicians, and so on, are insightful and readable. One terminological point that leaves me completely baffled is Pohlers' use of the word "folklore". The term is usually taken, if I'm not completely mistaken, to refer to results known by those in the know but not explicitly stated in the literature. Most results Pohlers terms "folklore" are certainly not folklore in this sense! (Or so I think, I haven't bothered to actually check this...)