Wednesday, July 29, 2009

Logic disappearing over the horizon ....

I've just had an invitation to give a talk at the University of X, a distinguished place, with a philosophy graduate community of about fifty (according to their website). So I checked out how much logic/phil maths is going on, what I could reasonably take as given. Zilch. Apart from a first year course perhaps approaching the level of my intro logic book, nothing at all, as far as I can tell. Which leaves me a bit bereft of anything to go to talk about. But more to the point, it means that for students at X a central swathe of the work of lasting value from the last hundred years has disappeared over the horizon. Which is, shall we say, a pity.

My sense is that this is happening more and more in UK universities. I'd be delighted to learn that I'm wrong.

Saturday, July 25, 2009

World-class again

I got the very good news eight or nine days ago of an award under the AHRC Research Leave scheme, to complete a book on Gentzen's proof(s) of the consistency of arithmetic (how the best versions work -- not obvious -- and what their philosophical significance is -- not at all obvious). As quite a few people have said to me, there's a very real need for such a book, and I hope I can make a decent job of it. I'm aiming to write something that is as accessible as my Gödel book as far as the technicalities are concerned (why is it that books on proof theory can be such tough going?); in other words, I want at least beginning grad students in philosophy who've done an intro math logic course to be able to follow it. And as for the philosophical commentary and critical discussion as we go along, well again I hope that will be accessible to the same audience too. (As my Explaining Chaos and Gödel books should show, I'm all for maximum accessibility: there's no point in trying to write a book for a readership of eleven, if only because no publisher these days would touch it.)

Now, I posted here a week ago, saying that I'd got the grant (and praising the AHRC for a conspicuous lack of ageism). But I added a remark -- in what was supposed to be tone of world-weary amusement -- about the fact that my research proposal was ranked "an outstanding proposal meeting world-class standards of scholarship, originality, quality and significance", suggesting that "world-class" was going it a bit.

Where two or three philosopher are gathered together these days, we often bemoan the exaggerations that have become routine in writing references, commenting on grant proposals, etc. etc. A student, to get into a US grad school, has to be the best you've taught in a dozen years; a planned piece of work has to be of ground-breaking originality, with the world waiting breathlessly. (In fact, I wrote here about reference inflation just a few weeks ago: we all know the phenomenon only too well).

Well, I don't know about you, but to me "world-class" means really, really, outstanding. How many world-class philosophers are there active in the UK? How many would you put into your world first eleven? Ok, let's be generous, your world first twenty-five all-stars? The fingers of one hand would be enough to count them, surely.

And one thing is for certain, by my lights most of us who get AHRC grants are not "world-class". We are trying to usefully move things on just a bit; we hope our stuff might get onto reading lists and get talked about a bit in its area. In other words, we try to be decently interesting and make some good new points. But in my idiolect, as in that of most philosophers, that hardly makes the work discipline-changing world-class stuff.

So, I said I was amused by the seeming gap between "world-class" and the useful, pushing-things-on-a-bit book that I'm writing. And I lamented the way that exaggerations of that kind have become rife in political and management discourse (ok, I used that philosopher's term of art "bullshit").

Well, what was supposed to be a weary old lag's comment on a linguistic decline has apparently caused serious offence. In particular, it has been suggested that describing my planned book as doing for Gentzen what I tried to do for Gödel, i.e. "explain clearly and make a few philosophical comments along the way" was inconsistent with its being proper research, with the implication that I shouldn't be getting the grant and had been deceiving the AHRC. But "making a few philosophical comments along the way" was of course exaggerating in that understated Cambridge way, to counterbalance the "world-class" exaggeration in the opposite direction. So I do apologize if someone got the wrong end of the stick. Of course what I'm doing is serious business, pushing things on as best I can. That should go without saying: but it seems that I need to say it.

Ok, back to thinking about provably terminating computations ...

Wednesday, July 22, 2009

Congratulations to Wilfrid Hodges!

Logicians will be delighted to see that Wilfrid Hodges has been elected a Fellow of the British Academy.

One to cross off your list

Suppose an undergraduate wrote this:

The first [incompleteness theorem] says that there are truths of arithmetic that are not provable in a consistent first-order logic that can express arithmetic.
You'd patiently explain that there are four things wrong with this. First, it confuses "logic" with "theory". Second, as you'd remind the student, the first theorem was originally proved for a higher-order theory, and applies to any theory which is properly axiomatized, whether first-order or not. Third, this statement confuses the conditions for semantic and syntactic versions of the first theorem. If you only assume the theory can express enough arithmetic, then you need to assume soundness to derive incompleteness; if you only assume consistency, as in the standard syntactic version, then you have to assume that the theory can represent enough arithmetic (where this is a matter of proving, rather than merely expressing, enough). And fourth, the statement is fatally ambiguous between (a) there are truths not provable in any consistent theory which can represent enough arithmetic, and (b) for any consistent theory etc. there are truths that that theory can't prove. Given that folk misinterpretations of Gödel trade on that ambiguity, you drill into your students the importance of clearly avoiding it.

Your student goes on to write:
The standard view is that we cannot prove CON(PA), period. (I use CON(PA) as an abbreviation for the sentence that expresses the consistency of Peano Arithmetic.) ... However, all that follows from the Gödel theorems is that we cannot prove CON(PA) with mathematical certainty.
Again, you'd start by patiently reminding the student that there is no such thing as the sentence that expresses the consistency of Peano Arithmetic -- and that matters because, as Gödel himself later observed, there are sentences that arguably in some sense express the consistency of PA which are provable in PA. In headline terms, it matters for the Second Theorem which consistency sentence you construct, in a way that it doesn't matter for the First Theorem which Gödel sentence you construct. But second, and much more importantly, it certainly is not the standard view that we cannot prove CON(PA), period. Any good treatment emphasizes that unprovability in PA is not unprovability period. Third, you'd add that it doesn't follow from Gödel theorems either that "we cannot prove CON(PA) with mathematical certainty". What's wrong, for example, in proving CON(PA) from PA plus the Pi_1 reflection schema for PA? If you are mathematically certain about PA and its implications, why wouldn't you be equally certain about the result of adding instances of the reflection schema? Arguably you should be: but in any case, nothing follows from Gödel theorems about that issue. And fourth, you might quiz your student about what he makes of the Gentzen proof.

Ah, he says,
We need transfinite inductions along a well-ordered path of length epsilon_0 to prove CON(PA) [in Gentzen's way]. The issue, then, is this: if human minds know the truth of CON(PA) with mathematical certaintly, is the only method by which we do it the use of infinitely long derivations?
But there seems to be a bad misunderstanding here: you'd remind your student that a proof by transfinite induction is not an transfinitely long derivation: it is just a proof assuming that a certain ordering is well-founded.

Unfortunately, those quotations -- and there's more of the same -- are not from a student essay but from a book, one published by MIT Press no less, Jeff Buechner's Gödel, Putnam, and Functionalism (see p. 8 fn. 8; p. 33; p. 39). The book turned up as I dug through the archeological layers on my desk in my Big Book Clear Out: I was sent it some time ago to review. But with garbles like that in a book one of whose main topics is the implications of Gödel for functionalist mechanism about the mind, I'm not encouraged to read any further. Life being short, I probably won't.

Added later: The Reviews Editor is twisting my arm in a flattering kind of way. Maybe I will review this after all.

Friday, July 17, 2009

Time-travelling with Google maps

Late last night, I walked down the street where I lived from the age of four until I was fourteen. A virtual walk, using Street View in Google maps. A rather sad experience though. For what a visual mess so much of the English urban landscape has become!

When I lived there -- we are talking about the outer London suburbs in Surrey -- the streets were quietly respectable, each house (built in the 30s, I think) separated from the road by a small front garden, neatly enclosed in privet hedges, with the obligatory flowerbeds and small patch of lawn. The houses along the road were identical apart from the colours of the front door. No one could call them particularly elegant. But there was a quiet uniformity; and the trees along the grass verges to the road, together with the hedges and front gardens, softened the rather dour drabness of the brick houses, so the overall effect was pleasing enough. As home-owning (as opposed to renting) became more common among the middle middle classes after the war, it was just the kind of street people aspired to live in.

Now, of course, the hedges and front lawns and hollyhocks have nearly all gone: where there were gardens, there is concrete and asphalt and paving stones, so cars can be parked two abreast with their noses up against the front windows. The long green verges to the road have been paved over too, so people can drive their cars across, with the few remaining trees isolated on little patches. The houses themselves have suffered from scattered cheap replacement windows, a new porch here, a differently tiled roof there. It all looks more than a bit scruffy: there is nothing along the road to soothe the eye, no riots of flowers to cheer the heart. I can't imagine anyone positively aspiring to live there.

Yet the houses now change hands for a third of a million pounds.

Tuesday, July 14, 2009

Twitter is sometimes not entirely frivolous

I was amused by the kids twittering away at the Joint Session (like third-formers passing notes in the back row) -- some very good pics too. Mildly fun to see what I was missing. If not exactly useful.

However, a recent tweet from Robbie Williams did very interestingly point out that the first vol. of Saul Kripke's papers has been announced. I'll believe it, though, when I see it.

Monday, July 06, 2009

Gödel sorted ... until the next time

Well, I've just this morning sent off the PDF for the next reprinting of my Gödel book: it should be available mid-August. I've eliminated quite a few more typos (thanks to everyone who let me know of errors in the earlier printings), made a scattered selection of small clarifications/stylistic improvements, and corrected the major errors that were still lurking even in the first corrected reprint. The biggest change is the one I mentioned a couple of posts ago, concerning Rosser's Theorem.

Being a reprint though, I couldn't change the "extent" of the book, the number of sheets that need printing. (Fortunately, the previous version finished on a recto page, so I had the verso to play with, and needed the extra side to correct the treatment of Rosser's Theorems). But given a new edition, I'd like another dozen or fifteen pages. First, I'd give a nicer proof that Robinson Arithmetic can capture all p.r. functions. Second, I'd fill in all the details of the proof that Prf(m, n) is p.r. (the final stages of which are just sketched). Third, I'd fill out the proof of the derivability conditions for theories with a smidgin of induction (again, I give an arm-waving sketch). As to the second and third, I originally didn't worry about giving sketches, as filling out the details is pretty tedious and unexciting (what you surely want to get across are the proof-ideas: and I referred masochists and completists to places where they can get the full gory story). But a number of readers have thought I should have gone the extra mile and risen to the challenge of giving full, though still maximally accessible, proofs. OK: if there's a second edition with a slightly longer page budget I'll have a bash ... But that will have to wait a bit.

Apple Preview: fail

This might just save a few Mac-based LaTeX users some grief. Suppose you use TeXShop to typeset

\documentclass[11pt,a4paper]{article}
\begin{document}
$\{0\} \to \{y = 0\}$
\end{document}
The result looks just fine in the TeXShop preview window onscreen (which calls on the Mac pdf Preview engine). But print it out and the spacing after the arrow is wrong. You get
{0} →{ y = 0}
Use Adobe Reader to print the pdf and all is well:
{0} → {y = 0}
The problem seems to be that the use of '}' as a printing character before a binary operator can mess up the printing though not the viewing of a pdf by Preview. Very, very odd. But apparently there are other known issues with Preview printing pdfs and missing/misplacing symbols. So the moral is: when it matters, print using Adobe Reader.

Stumbling over the bug caused me some hours of annoyed and mystified head-scratching. The invaluable comp.text.tex newsgroup helped me find a minimal example and pin the blame on Preview rather than on my (occasionally ropey) LaTeX coding.