Getting categorical

For a bit of light relief from matters Gödelian, I’m hoping to spend the next couple of months getting more to grips with category theory (well, and why not? — there are world-class category theorists just down the road at CMS, Martin Hyland and Peter Johnstone for a start, and it might be fun to be able to sit at the back of the category theory seminar and have some sense of what is going on). So I’ve gathered a somewhat daunting stack of books, and am plunging in … I’ll report progress!

Meanwhile, over 250 people have downloaded the Gödel book, and I’ve already had some very useful comments. In particular, Toby Ord has quite rightly taken me to task for getting a bit overexuberant in saying of Section 33.5 that it gives a proof that the Church-Turing Thesis entails the First Incompleteness Theorem. What the section does, in fact, is take the Kleene Normal Form Theorem and deduce incompleteness, assuming CTT along the way. But like any appeal to CTT in proving a formal result, that’s a labour-saving device that is dispensable — and if it weren’t, we’d be able construct a related counter-example to CTT (as I’d already pointed out in Section 28.7). So really, I guess I should have said, less dramatically, that KNFT entails incompleteness. Still, it’s a lovely argument if you don’t know it: and the point remains that in thinking about CTT, and proving recursiveness is equivalent to Turing computability as a step in its support (and that equivalence yields KNFT very easily), then we get incompleteness almost immediately — and that’s surely a nice surprise!