Gödel, Lean, Fra Angelico, Schubert
So far – but then I am still in the foothills, tinkering with early chapters – I have found just a couple of minor expositional stumbles in An Introduction to Gödel’s Theorems. I have spotted, though, quite a few places where I can make the text run just that bit more smoothly. And my friend Gemini Pro has also chipped in with perhaps two or three helpful small suggestions per chapter.
There is just one passage in the book, however, which now strikes me as just wrong. It’s not a technical error (phew!). But I do write on p. 25, talking about projects of formalization, that “outside the logic classroom we almost never set out deductive arguments in fully formalized versions”. That was perhaps more or less true enough when I first wrote it about twenty years ago; but it certainly isn’t today, with the exponential growth of work using formal computer proof assistants like Lean.
So I have just been looking around for a reference or two to Lean and its cousins for a possible footnote. And I found this piece by Jeremy Avigad and others which appeared last year in Notices of the AMS, which I thought was enlightening and might be of wider interest.
I’m much enjoying getting back into thinking a little about Gödelian matters. And as I get to the point of revising the main chapters on the arguments for the first incompleteness theorem, one task for me will be actually to read Gödel 1931 again to see if I want to add more references to the paper. I must also take another look at the volume Jan von Plato published in 2020, as the result of his detective work grappling with Gödel’s shorthand notes written in the months leading up to his publishing the epoch-making paper. (Apart from a review by John Dawson in Philosophia Mathematica, that volume seems to have received surprisingly little attention. Perhaps because it does seem to take some effort to dig out the more interesting material – I’ll perhaps write something brief about that here.)
So it turned out that we couldn’t get to the Fra Angelico exhibition at Palazzo Strozzi and the convent of San Marco. By all accounts, it was wonderful to see – there is a very readable piece by Anna McGee in the London Review of Books here.
Getting the volume published to accompany the exhibition is – of course – a poor second best. Though it is wonderful to have. There are some very interesting essays. And you can revisit more often and can pause longer over some of the works in splendid illustrations (though the decisions over which panels and which frescos get really detailed reproductions are sometimes frustrating too).
But though the exhibition finishes, San Marco of course remains, and we must return one day. And as Anna McGee writes, “The convent and its art encourage a sort of contemplation different from that of a museum. Henry James, who visited in 1873, put it well: ‘You may be as little of a formal Christian as Fra Angelico was much of one, you yet feel admonished by spiritual decency to let so yearning a view of the Christian story work its utmost will on you.’”