Logic Matters

Catching up with Tim Gowers’s blog, I notice he makes some interesting remarks in passing about the idea of a proof. He’d initiated/co-ordinated a “polymath” project — a collaborative all-comers group effort trying to find a combinatorial proof of a result in Ramsey theory previously known from a proof in ergodic theory. After hundreds on contributions, but of course before any attempt to put the bits and pieces together into a conventionally written-up proof, Gowers says “I am basically sure that the problem is solved (though not in the way originally envisaged).”

Why do I feel so confident that what we have now is right, especially given that another attempt that seemed quite convincing ended up collapsing? Partly because it’s got what you want from a correct proof: not just some calculations that magically manage not to go wrong, but higher-level explanations backed up by fairly easy calculations, a new understanding of other situations where closely analogous arguments definitely work, and so on. And it seems that all the participants share the feeling that the argument is “robust” in the right way.

So, interestingly, getting a “correct” proof in his sense involves more than getting a proof in the austere logician’s sense of a correct proof as just (“magically”) getting out the desired result without logical gaps — it goes with explanations and understanding.

Let’s not fuss about terminology. It undoubtedly is the case that a notion of a correct proof in something like Gowers’s sense functions centrally in mathematicians’ thinking. But how good are the attempts by philosophers of mathematics to elucidate this notion?

Here, in a very slightly revised form — and I’m not going to have time to revise them properly for a while — are the handouts for three “Back to Basics” lectures on incompleteness that I gave at the Cameleon workshop a few weeks ago. There’s nothing excitingly original here, with the possible exception of mistakes! But maybe if you are looking for one story about the shape of the wood which doesn’t get too distracted by all the trees, then the handouts could be useful.

“To hear Mullova play Bach is, simply, one of the greatest things you can experience,” wrote Tim Ashley in the Guardian of a concert.

She’s now recorded the solo sonatas for the first time and re-recorded the partitas (this time using gut strings and a baroque bow on a stunning-sounding 1750 Guadagnini). I liked the previous recording of the Partitas a lot, and that was already one of my favourite versions. But this time the result I think is simply amazing, one of those recordings that immediately imposes its vision — compelling you to think this is how the music ought to be played. It is indeed a great thing.

Steve Awodey has a quite short but fascinating paper now available online called ‘From Sets to Types to Categories to Sets’, inter alia saying something tolerably accessible about the significance of his recent technical work. Here’s the first paragraph:

Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby.

And here’s the last paragraph. Awodey has been noting the set theory gives constructions features that are not mathematically salient — ‘no topologist or algebraist is concerned with the logical type or ordinal rank of a manifold or module’ — though ‘they can serve a useful purpose in foundational work by providing the concrete data for specifications and calculations, facilitating constructions and proofs.’

By contrast, the purely structural approach of category theory sometimes offers comparatively little such “extra” structure to hold on to. Practically speaking, it can be harder to give an invariant proof. That is why it’s good to know that such logical structure can always be introduced into a category when needed; the devices of introducing an internal logic or a set theoretic structure into a category, as sketched in the foregoing sections, were originally developed in order to benefit from their advantages, much like introducing local coordinates on a manifold for the sake of calculation. The analogy is quite a good one: no one today regards a manifold as involving specific coordinate charts, and one generally works with coordinate free methods so that the results obtained will apply directly|this is the modern, structural approach. But at times it can still be useful to introduce coordinates for some purpose, and this is unobjectionable, as long as the results are invariant. So it is with categorical versus logical foundations: category theory implements the structural approach directly. It admits interpretations of the conventional logical systems, without being tied to them. Category theory presents the invariant content of logical foundations.

Anyone interested in foundational issues will want to read the paragraphs in between the first and last! (Thanks to Richard Zach, over at LogBlog, for the link.)

At long last, the much corrected reprint to my An Introduction to Formal Logic (CUP, originally 2003) has arrived on my desk and is in stock at the publishers. It’s been a bit of a saga, but worth the effort. All the needed corrections which I originally listed on the web pages for the book have been made, and there are dozens of other small improvements scattered through the book.

Students: it will be much less irritating getting the corrected version even if it costs a bit more than a second-hand copy of the first printing. The paperback is relatively cheap anyway, and the new version is significantly better.

Colleagues: if you are using the book to teach from, don’t worry. Even though the new version is an improvement, and some things are better explained, you won’t have to change your lectures and classes much if at all!

Phew! Well, thank heavens that’s over. I just hope it is more than three days before I notice the first misprint in the new version …

This is only going to be of interest to locals (or those passing through Cambridge). But I warmly recommend Alimentum. The best meal out we’ve had in Cambridge, ever. By miles. In fact the best meal out since we were last in Italy. Modern euro style — fantastic quality venison, beef. Share a plate of the cheeses too before moving on to dessert. The wine was quite excellent as well, though I’m not going to say what we drank, in case that means people finish up their stock! — but let’s just say that Gambero Rosso were right about it.

Note to students: this has to be the place to get your ever-loving visiting parents to take you to, if they are used to London prices and won’t curl up in shock (though The Daughter, who has dined out a lot in London, thought Alimentum compared well with many supposedly classy London places).

I was wondering whether to spruce up my very rapidly written hand-outs on Gödel’s Theorems which I produced for the Cameleon weekend and publish them here. I was beginning to think I wouldn’t bother, as there are other things I want to be getting on with. But I just now read the chapter on incompleteness in Shawn Hedman’s A First Course in Logic, and that reminded me how crummy some textbook treatments can be, and hence of the need for crisp and clear presentations. Not that Hedman is technically wrong, of course (well, I haven’t read him that carefully, but the details look ok). But I defy any beginning student to take away from his chapter a really clear sense of what the key big ideas are, or of how to distinguish the general results from the hack-work needed to show that they apply to this or that particular theory. So back to those hand-outs!

I’ve just uploaded a new version of the corrections sheet for my Gödel book, at www.logicmatters.net. I’m still cogitating how best to handle some further suggestions/complaints (and how best to respond to nagging worries I have about my presentation of the Second Theorem) — but I thought I should at least upload an interim report while I was in the mood to get at least some of the job done.

I hope I’ll eventually have the chance of another corrected reprint. Part of me would like a whole new edition; there’s stuff I’d do differently now in ways that would require more than local changes. But new editions aren’t always better (for the temptation is to pack in more material, and the book is already too long).

It’s all been getting a bit monochrome and serious here lately (memo to self: lighten up a bit). So as a distraction from the rigours of logic here’s another in that occasional series of photos of Monica Vitti. This one — click to enlarge — was taken in Rome by the photographer Willy Rizzo in 1960, the year of L’avventura, when she was 28.

A lot has been written about that elusive film: this, by the critic Gregory Solman, perhaps gets something right about it.

I don’t get to the cinema much these days: but I wonder what comparable films are being made that can and will be watched, repaying the same serious attention, almost fifty years on. Any suggestions?