Year: 2022

GWT2 — a first full draft

I now have put together a first complete [updated, now third] draft of the second edition of Gödel Without (Too Many) Tears. You can download it here.

I need to do a careful read-through for typos/thinkos. I also need to update the index, make the typography more uniform between chapters, and e.g. decide on a more consistent policy about when I cross-reference to IGT2. That sort of fun to come over the next month or so. I’ll post updates from time to time, and the link above will keep pointing to the current draft version of GWT2.

It is too late to write a very different book, and after all this is supposed to be just a revised edition of the seemingly quite well-liked GWT1! This is not the moment, then, for radical revisions. But otherwise, all suggestions, comments and corrections, including quick notes of the most trivial typos, will be most welcome! Send to the e-mail address on the first page of PDF, or comment here. (Just note the date of the version you are commenting on.)

Actually, many readers of this blog will have better things to do than spend much time with this sort of intro-level enterprise (though massive thanks are due to a handful who have already been e-mailing comments). But if you aren’t a student yourself, you could well have students who would be interested to take a look and let me know what they find too obscure, and/or give other comments and corrections. (Back in the day, I lined up a whole team of volunteers to look at a couple of chapters each of IGT2: and there turned out to be precisely zero correlation between “status”, from undergraduate to full professor, and the usefulness of comments!) So do please spread the word to any students, undergraduate or graduate, who might be — or ought to be! — interested.

It’s not much of a bribe, I know, but those impoverished students who prompt the biggest corrections/improvements will get a free paperback in due course, as well as having their name in lights in the Preface!

Added: Latest version, linked above, Thursday 12 September.

PHQ, at the Edinburgh Festival

Photo by Petra Hajska

There was an extraordinary concert by the Pavel Haas Quartet at the Edinburgh Festival on Tuesday morning, with a BBC radio recording available for a month. They gave very fine performances of

Haydn: String Quartet in G major Op. 76/1
Martinů: String Quartet No 7 H314
Schubert: String Quartet in G D.887

The Schubert was particularly intensely felt. But what made the performances little less than miraculous was that they playing with (yet another) new violist. The gifted Luosha Fang was with them as recently as the East Neuk Festival in early July; and interviews when their Brahms Quintets disk came out a bit earlier gave every impression that after a year she was very much part of the Quartet. But now, it seems, more trials and tribulations for the Quartet and, for whatever reason, a sudden parting of the ways. The viola seat is now being occupied — at least for the rest of the year — by a Czech compatriot, Karel Untermüller. So there he was, just a few weeks into the role: yet the ensemble seemed (at least to my not very expert ears) to be as remarkable as ever. Which, as I say, was surely rather extraordinary.

There is a good piece on the concert here.

Added And there is now also a rave review here. It finishes “These musicians are at the very top of their form: their playing is virtuosic, their tone is sensational, and they listen to one another as though their lives depend on it. In short, wonderful.” Perhaps it was the very necessity of extra-extra-close attention to each other, playing with a brand new member, that produced  such fine performances.

NF is consistent

Randall Holmes has been claiming a proof for about a decade, and recently posted yet another improved update of his proof on arXiv.

A while back, there was some very interesting discussion about the possibility of formalising the proof using a proof assistant like Lean. There’s now some relevant local news, which I get from Thomas Forster.

Roughly speaking, the proof has three components. (1) Randall proved over twenty-five years ago that NF is consistent if what he called Tangled Type Theory, TTT, is. Arm waving, if a sentence S is a correctly typed sentence of the simple theory of types, and S^* is what you get by replacing the type levels in S with new type levels with the same order relation, then S^* is a sentence of TTT. So where in the simple theory, for x \in y to be well formed, y has to be one type higher than x, in TTT x \in y is well-formed even when y is more than one type higher than x, so there is an \in relation between any lower level and any higher level. This relative consistency claim of NF and TTT is unproblematic.

(2) TTT is a seemingly rather wild theory (Holmes calls it “weird”). But Holmes now aims to present a Frankel-Mostowski-style construction that purports to be a model of TTT. The devil is in the contorted(?) detail: do we get a coherent description of a determinate structure?

(3) Assuming that stage (2) is successful in at least describing a kosher structure that a ZF-iste can happily accept as such, there then is the task of verifying that it really is a model of TTT.

Now, over the last few weeks, a bunch of maths students here have been working on a summer project arranged by Thomas (with a lot of Zoomed input from Randall) to formally verify the consistency proof in Lean, by first checking (2) that the model is coherently constructed, and then going on to check (3) it really is a model of TTT. And I understand the state of play to be this: that first of these stages is successfully more or less completed. And it has in the process become intuitively clear — said Thomas — that the defined structure is indeed a model of TTT. Dotting the i’s and crossing the t’s and implementing a Lean check that the model satisfies a certain finite axiomatization of TTT will take more time than there is left in this summer’s project (the students have lives to lead!). But with (2) secure, it looks as if Holmes indeed has his claimed proof, though its final best-form shape remains to be settled.

If that’s right, Holmes has settled one of the oldest open problems in set theory. Though quite what the wider significance of this, I’m frankly not so sure. Will a consistency proof (of a decidedly tricksy-seeming kind) really make us look much more kindly on NF? Should it?

GWT2 — up to the first incompleteness theorem

I have now revised Gödel Without (Too Many) Tears up to and including the pair of chapters on the first incompleteness theorem. You can download the current version up to Chapter 13 here.

For info: the chapter on quantifier complexity has been revised (adopting a more complex definition of Sigma_1 sentences, so that I don’t have to cheat later in saying that primitive recursive functions can be defined by Sigma_1 sentences). Then the chapter on primitive recursive functions has been slightly revised yet again. I have tried to make the chapter that proves that primitive recursive functions can indeed be defined by Sigma_1 sentences a bit more reader-friendly (the key ideas are elegantly simple: implementing them is unavoidably a bit messy). The chapter on the arithmetization of syntax is little altered. And finally in this instalment, the two chapters on the semantic and syntactic versions of the first incompleteness theorem are more or less untouched.

I’m still on track for getting a second edition out by around the end of October. It goes without saying that all comments and corrections will be gratefully received (and do please alert any students who might be interested in reading through and spotting typos or unclarities). Many thanks once again to David Furcy and Rowsety Moid for corrections and suggestions.

Added 24 Aug Corrected version uploaded.

IFL as a free download, two years on …

The second edition of my An Introduction to Formal Logic was originally published by CUP. It is now exactly two years ago today that I was able to make the book free to download as a PDF and also make it available as a very cheap paperback, thanks to the Amazon print-on-demand system. How have things gone?

As with the Gödel book I really didn’t know what to expect. But from almost the beginning, IFL2 has been downloaded about 850 times a month, and has sold very steadily over 75 paperbacks a month (with numbers if anything creeping up). Which, on the one hand, isn’t exactly falling stone-dead from the press. But, on the hand, given the very large number of philosophy students who must be taking Logic 101 out there in the Anglophone world, it isn’t an overwhelming endorsement either. However, you can’t please everyone: there isn’t much consensus about what we want from an intro logic book (which is why unwise lecturers like me keep spending an inordinate amount of time writing our own, despite the best advice of our friends …). Modified rapture, then.

So what now? IFL1 was truth-tree based. IFL2 uses a Fitch-style natural deduction system. The intro book I’d ideally write would cover both trees and natural deduction. That wasn’t possible within the CUP page budget. But those constraints are lifted. A PDF can be as long as I want; and in fact the marginal additional printing cost of expanding the paperback by fifty or sixty pages wouldn’t make very much difference to the price. So an expanded IFL3 is certainly a possibility. But do I actually want to write a third edition?

OK, I confess I’m tempted! Not at all because I think the world stands in desperate need of such a book, but because (very sad to relate) I’d actually rather enjoy the exercise of getting things into the best shape I can, before I hang up my expository boots. A plan for 2023? If the gods are willing.

Reasons to be cheerful, of a reading kind

Janus La Cour, Olive Trees Near Tivoli

To the Fitz, to see their exhibition (on for another twelve days) “True to Nature”. Which we very much enjoyed (rather to our surprise, much more so than the trumpeted Hockney exhibition which is still continuing). Mostly minor works, to be sure, but the cumulative affect a delight, with some gems you would be more than happy to live with. Like these gnarled olive trees.


A list of forthcoming autumn books in one of the weekend papers. At the end of this month, we get Maggie O’Farrell’s The Marriage Portrait. “Winter, 1561. Lucrezia, Duchess of Ferrara, is taken on an unexpected visit to a country villa by her husband, Alfonso. As they sit down to dinner it occurs to Lucrezia that Alfonso has a sinister purpose in bringing her here. He intends to kill her.” OK, you’ve got me! I thought Maggie O’Farrell’s Hamnet was wonderful: so can’t wait for this. Then Elisabeth Strout has another novel, fast on the heels of the marvellous Oh William!: in October we get a sequel,  Lucy By The Sea. Then, not least, there is a new Kate Atkinson coming, Shrines of Gaiety. Enough said! Some happy autumn evenings ahead. Three reasons to be cheerful.


I was struck that the ones that stood out for me in that list of autumn books were all by women. And looking back at the list I keep, I see that most of the two dozen novels I’ve read this year so far have been by women. At least of the recently published ones, only one was by a man — Julian Barnes’s Elisabeth Finch. I must be missing out on something: but what?


A book taken down from the shelves one recent evening, The Faber Book of Landscape Poetry (a serendipitous as-new Oxfam purchase a while back). A real pleasure to dip into — some very engaging poetry, some familiar, some not at all. Perhaps not very challenging. Indeed, to be honest, perhaps a rather conservative selection. But then it was edited by a conservative, indeed a Conservative politician, the one-time Education Secretary Kenneth Baker. The thought strikes: which of the last six or seven Conservative Education Secretaries might have even had any literary interests, let alone sensibly edited some such book? Anyone?


Another forthcoming book: A. E. Stallings This Afterlife: Selected Poems. Something else to really look forward to. Pleasures of the reading kind will be plentiful, then. Outside books, the world isn’t doing so well, is it?

IGT as a free download, two years on …

I’ve just noticed that it is almost exactly two years since I was able to make An Introduction to Gödel’s Theorems, originally published by CUP, freely available to download as a PDF.

After a ridiculously large initial flurry of downloads, the book is now steadily downloaded about 600 times a month. As I’ve said before about such stats, it is very difficult to know how to interpret the absolute numbers: but this looks respectable enough, and  the trend is still upwards.

When I originally announced, without much fanfare, that the PDF was available, I added

I may in due course also make this corrected version of the book available as an inexpensive print-on-demand book via Amazon, for those who want a physical copy. But I doubt that there would be a big demand for that, so one step at a time

Well, of course, I soon did set up the POD paperback (very easy if you already have a publication-quality PDF), and I was proved quite wrong about demand. I thought any sales would be a tiny trickle given the availability of a completely free download; but in fact the paperback of IGT very steadily sells over 50 copies a month, over three times as many it was doing under the auspices of CUP. So I think we can count the experiment as a success!


Back in the day, when I was writing the first edition of IGT, I tried to do the whole thing from memory, reconstructing proofs as I went, on the principle that if an idea or a proof-strategy had stuck in my mind, then it was probably worth including,  and if it hadn’t then maybe not. I did fill in some gaps once I had a complete good draft; but that explains the relative shortage of footnotes to sources. When I look at the book occasionally, it is just a tad depressing to realize that I would struggle to rewrite it from memory now. That struck me forcefully yesterday when, reworking a section in Gödel Without (Too Many) Tears for its second edition, I consulted IGT and came across an important point that, at least for the moment, I’d quite forgotten the intricacies of. Ah well …

GWT2 — on primitive recursive functions

I have recently been re-reading Wuthering Heights, for the first time in however many decades. I’m not sure what prompted me to reach the book down from the shelves, and I wasn’t sure either how I would take to it in my dotage. Isn’t it a book for the young and over-romantic? Yet I am engrossed and carried away. What passionately driven writing! Utterly extraordinary. But you knew that.

Should I be surprised that Emily Brontë’s teacher in Brussels wrote of her “She had a head for logic, and a capability of argument unusual in a man and rarer indeed in a woman …”?

Back to logic for me. And so here is the revised chapter on primitive recursive functions from GWT2, just 11 quick pages. Some from a more computer science background complained a bit about what I wrote in the previous edition (and should indeed be similarly dissatisfied with the similar treatment in IGT2). I have, in particular, tried to make the passing remarks about “for” loops and “do while” loops less misleading. Have I succeeded?

Updated (with thanks to RM for his comment).

Jeunes Etoiles

Having just grumpily posted about a disappointing logic book, now for something the very opposite of disappointing …

The Gstaad Digital Festival has been streaming a series of concerts by young musicians, “Jeunes Etoiles”. The latest was a terrific concert by the cellist Friedrich Thiele wonderfully accompanied by  Elisabeth Brauss. They played Beethoven’s variations on Mozart’s «Bei Männern, welche Liebe fühlen», Schumann’s Fantasiestücke for Cello and Piano, and five Shostakovich piano Preludes arranged for Cello and Piano followed by his Cello Sonata Op. 40. All the Shostakovich was new to me and I was very taken with the music. All extraordinarily well played to my ears — and as you can see, the performers too seemed really delighted by how the short concert had gone. Here’s a link to them.

(Another) one to miss …

If any title in the Cambridge Elements series was especially designed to catch my interest, it would be Theoretical Computer Science for the Working Category Theorist. Not, of course, that I am in any sense a ‘working category theorist’, but I’m certainly interested, and know just a bit. And I know a smidgin too about computability theory. So I, for one, should be an ideal reader for an accessible short book which sets out to give more insights as to how the two are related. The introduction notes that there are a number of texts aimed at the computer scientist learning category theory (like the excellent Barr and Wells, Category Theory for Computing Science); but Noson Yanofsky promises something quite different, aimed at someone who already knows the basics of category theory and who wants to learn theoretical computer science.

It most certainly didn’t work for me. The author has a line about the central relevance of the notion of a monoidal category here, but makes it quite unnecessarily hard going to  extract the key ideas. Indeed, overall, this  just strikes me as very badly written. Careless too. What, for example, are we to make of slapdash remarks like “the German mathematician Georg Cantor showed that sets can be self-referential” or “Kurt Gödel showed that mathematical statements can refer to themselves”? (And on Gödel, I doubt that anyone who isn’t already familiar with the proof of  Gödelian incompleteness theorems from the unsolvability of the Halting problem is going to get much real understanding from the discussion on pp. 71–72.)

I could go into a lot more detail, but to be honest I found the book far too disappointing to want to put in the effort required to disentangle things enough to make for useful comments. Sorry to be so negative. And your mileage, of course, might vary …

[Also see Peter F’s comment.]

Scroll to Top