Two category theory books

One of the best freely available sets of lecture notes on category theory available is the one by Paulo Perrone, which can be downloaded from the arXiv here. He has now turned these notes into a printed book, Starting Category Theory from World Scientific. There is a long added chapter on monoidal categories, but the earlier five chapters appear again with only some small additions as far as I can see on a quick browse (the significantly higher page count for these chapters being mostly due to the difference in formatting).

Since the lecture-note version is freely and officially available, I won’t comment in detail here: suffice to say that Perrone makes the material pretty accessible, and I can well imagine many students liking his style. I really, really doubt that they (or you) will want to fork out for the book, however. Its USA price is $148 (there’s a whopping $11 discount on Amazon); its UK price is £135. That is worse than absurd.

I may just possibly have said something here about another category theory book’s being on its way. Namely, my Category Theory II. But plans are a bit fluid right now. For various reasons, I’m increasingly minded to in fact combine Parts I and II (with again a slightly re-arranged ordering of chapters) into a single big book, perhaps reverting to that earlier title Category Theory: Notes towards a gentle introduction for the whole.

In fact the cost of one big printed book would only be about the price of a large coffee more than a separate Category Theory II, and the small additional overall cost to someone who already has Category Theory I would be more than compensated by avoiding the repeated annoyance of having to chase up cross-references between books (or between PDFs). And there are other significant potential gains too: the combined book as I now see it has a nicer shape. But I’ll keep thinking this through: so watch this space.

Timothy Chow on the NF consistency proof and Lean

Timothy Chow has sent a long comment, adding to the discussion following the previous post NF is really consistent. I think the points he makes are interesting enough to highlight as a standalone guest post. He writes:

First, let me congratulate Randall and Sky on a magnificent achievement!

I’m afraid I have to agree with Randall that the likely response of the mathematical community is a polite yawn. That is unfortunate, because there are several reasons why people should be excited about this work.

The first reason is simply that a difficult, well-known, and longstanding conjecture has finally been proved, via a brilliant argument that uncovers deep structure in an unexpected place. I don’t know what mathematics is, if not the uncovering of deep and unexpected structure. If the subject in question were anything other than mathematical logic, which many mathematicians are unjustly prejudiced against, the champagne corks would already be popping.

Even many set theorists seem to be prejudiced against NF. There are standard complaints that it presents a strange and unmotivated foundation for set theory. But as you can see from older papers on his webpage, Randall has long ago addressed these objections. The time is long overdue for a re-evaluation of the possible role that NF might play in the foundations of mathematics. Note that NF has type-theoretic origins; type theory is experiencing a renaissance of sorts nowadays, so it is especially appropriate for NF to be given a fresh look.

A second, and totally different, reason to be excited about this piece of research is that it convincingly demonstrates the value of proof assistants in the process of producing new mathematical knowledge. Not all readers of this blog may be aware of the history of this proof of the consistency of NF. Randall announced the result over ten years ago, and submitted a paper for publication, but the editor did not want to publish it until a referee could be found who was able to independently vouch for its correctness, and no such referee was forthcoming, because the proof was so complicated. This state of affairs highlights one of the weaknesses of our peer review system; if a proof is very complicated and there is uncertainty about its correctness, then referees are typically reluctant to invest a lot of time checking it, because if the proof turns out to be wrong, then they will likely have wasted a lot of time that they could have spent pursuing more rewarding activities. People don’t want to read the proof until they’re sure it’s correct, but there’s no way for the proof to be recognized as correct until people read it. In the absence of a proof assistant, an author in possession of a correct but complicated proof is caught in a vicious cycle.

This is one major reason we should be grateful for proof assistants; they allow us to break the impasse. Rowsety Moid’s initial comment betrays a lack of understanding of this point. To say that the correctness of a proof rests on “the judgement of competent mathematicians who understand the proof” is partially correct, but fails to acknowledge that sometimes, human mathematicians are unable to arrive at such an understanding and judgment without machine assistance. Randall began with a basically correct proof, but the process of communicating the proof to other humans (which you might think is a purely human activity) turned out to be impossible until a proof assistant entered the picture. Furthermore, Lean did not simply play a purely passive role, dully checking a proof that had been completely spelled out by the humans in advance. As Randall will be quick to acknowledge, the process of coaxing Lean to certify the argument was not a monologue by the humans, but a dialogue that forced the humans to rethink, clarify, and improve the argument. Lean is truly an interactive proof assistant; we are entering a new era in which proof assistants are becoming vital partners in the creation of proofs, not just by performing routine calculations, but by engaging us in interactive dialogue.

Of course, some of these lessons were already learned with Flyspeck or Gonthier’s proof of the four-color theorem, etc. But a new feature of the proof that NF is consistent is that it demonstrates that what might seem to be a purely sociological issue (the difficulty of persuading a referee to check a proof and thereby allowing the proof to be assimilated into the body of accepted mathematical knowledge) can in fact be addressed with the help of an interactive proof assistant, which has infinite patience, and no pressing need to advance its own career by spending its time on more “important” tasks.

NF really is consistent

About eighteen months ago, I noted here that a project was underway to verify Randall Holmes’s rather impenetrable claimed proof of the consistency of NF, using the Lean proof verification system.

The project has now been completed by Sky Wilshaw, a Part III student in Cambridge, building on the earlier work of some other students. Here is a new paper by Holmes and Wilshaw explaining the proof in its current version. The introduction reads:

We are presenting an argument for the consistency of Quine’s set theory New Foundations (NF). The consistency of this theory relative to the usual systems of set theory has been an open question since the theory was proposed in 1937, with added urgency after Specker showed in 1954 that NF disproves the Axiom of Choice. Jensen showed in 1969 that NFU (New Foundations with extensionality weakened to allow urelements) is consistent and in fact consistent with Choice (and also with Infinity and with further strong axioms of infinity).

The first author showed the equiconsistency of NF with the quite bizarre system TTT (tangled type theory) in 1995, which gave a possible approach to a consistency proof. Since 2010, the first author has been attempting to write out proofs, first of the existence of a tangled web of cardinals in Mac Lane set theory … and then directly of the existence of a model of tangled type theory. These proofs are difficult to read, insanely involved, and involve the sort of elaborate bookkeeping which makes it easy to introduce errors every time a new draft is prepared. The second author (with the assistance of others initially) has formally verified the proof of the first author of the existence of a model of TTT, and so of the consistency of New Foundations, in the Lean proof verification system, and in the process has suggested minor corrections and considerable formal improvements to the argument originally proposed by the first author. The second author reports that the formalized proof is still difficult to read and insanely involved with nasty bookkeeping. Both authors feel that there ought to be a simpler approach, but the existing argument at least strongly resists attempts at simplification.

‘Quite bizarre system’, ‘insanely involved with nasty bookkeeping’ eh? There have been rather more inviting introductions to papers! But still, an insanely intricate and messy but verified-in-Lean proof of consistency relative to a fragment of ZFC is a consistency proof.

My strong impression, however, is that the general lack of love for NF among set-theorists hasn’t latterly been really grounded in lively doubts about its consistency. So I rather suspect that, even though the proof resolves a very long-standing open problem, its wider impact might be quite modest. Still, all credit to Randall Holmes for having brought his proof project to a successful outcome.

Jonathan Bennett (1930-2024), Michael Tanner (1934-2024)

The deaths have been announced of two Cambridge philosophers.

Jonathan Bennett was here from 1956–1968, and I was and remain a huge admirer. His early little book Rationality is a masterpiece, and for a good few years I was much intrigued by his defence of a Gricean programme in the philosophy of language which comes to fruition in his Linguistic Behaviour. And when it came to my retirement and I had to radically downsize my ludicrously big library, one of the few history of philosophy books that I couldn’t bear to let go was his Kant’s Analytic which still strikes me as the very paradigm of how to make the Great Dead Philosophers live as exciting interlocutors with something to say which is still worth grappling with. His energetic, direct, straight-talking style as a philosopher I found inspirational over the years.

Bennett was a prolific publisher, not so Michael Tanner, who spent his whole career in Cambridge, first as an undergraduate and then from 1961 until his retirement in 2002 as a lecturer. But he had a great cultural influence on many students over the years, in the way that dons of a different era could do. His Wagner evenings were legendary (and his eventual short book Wagner is a terrific read, even for those of us who never quite caught the bug). And he became a wonderful reviewer of CDs for the BBC Music Magazine, and of opera for the Spectator. He was passionately engaged, opinionated, insightful because — as a loyal Leavisite — he thought such things really mattered to life. (For some reminiscences, see the comments on Brian Leiter’s blog here.)

Category Theory I — now in paperback

Sound the trumpets! Or at least, let me give a small toot …

Category Theory I: A gentle prologue  is now available as a print-on-demand paperback. This is Amazon only (sorry, but that’s easiest for me and cheapest for you), with ISBN 1916906389, at £5.99, $8.25, €7.50. Those prices are only trivially rounded up from the minimum possible (e.g. from £5.90), so I’m not taking any significant royalties.

I’m thinking of the paperback as still a beta version of the text. Functional, and I hope with no horrible mistakes, but surely not bug-free. I’ll still be very happy, then, to get corrections and comments and suggestions for improvement. The Amazon print-on-demand system makes future updates of the file for printing very straightforward and cost free.

The PDF is of course still freely downloadable from the category theory page; but many prefer to work from a printed copy. So, since the paperback is the price of — what? — just three coffees, and is actually quite nicely produced, why not treat yourself!

Three things to read …

The death was announced a few days ago of W.W. Tait, whose work I have much admired over the years. His early technical work was on proof theory, and then he wrote with great knowledge and insight on the philosophy of mathematics and its history. His collection of papers The Provenance of Pure Reason is a must-read, and more excellent papers can be found on his otherwise minimalist website here. One piece of Tait’s which I can’t remember reading before and which will surely be of interest to anyone reading this blog is his piece contributing to Philosophy of Mathematics: 5 Questions: you can read it here.

Brian Leiter’s blog linked yesterday to a piece by a one-time colleague of mine, Leif Wenar, lambasting the pretentions of the “effective altruism” cult. I laughed out loud at his (surely just) comment that “To anyone who knows even a little about aid, it’s like [Will] MacAskill has tattooed “Not Serious” on his forehead.”. But this is serious stuff, and well worth a read here.

For some hard-core logical reading, here is another one-time colleague in action. Tim Button has just posted on the arXiv a forthcoming JSL paper “Wand/Set Theories: A realization of Conway’s mathematicians’ liberation movement, with an application to Church’s set theory with a universal set”. Tim describes a template for introducing mathematical objects which prima facie is much more liberal than standard set theory provides. Indeed it seems to very nicely encapsulate Conway’s liberation movement, allowing that (in Conway’s words)

(i) “Objects may be created from earlier objects in any reasonably constructive fashion.

(ii) Equality among the created objects can be any desired equivalence relation.”

Note, though, that Conway expected that any theory whose objects are so created in such a “reasonably constructive” fashion can be embedded within (some extension of) ZF. Tim aims to prove a stronger theorem: all loosely constructive implementations of the Wand/Set Template are not merely embeddable in (some extension of) ZF, but synonymous with a ZF-like theory. Which seems a surprise.

Markdown joy

A minor improvement here …

You can now use simple Markdown syntax (you know the kind of thing, *italics* for italics, **bold** for bold) in comment boxes.

This is explicitly signalled in comment boxes on the blog; but it is also the case with comment boxes on static pages.

(Nerdy trivia: this is enabled by using the multi-purpose Jetpack plugin — which is wild overkill: but I’ve turned off more or less every other Jetpack option so I hope that nothing is inadvertently broken.)

Elisabeth Brauss at Wigmore Hall

A wonderful lunchtime concert by Elisabeth Brauss at Wigmore Hall this Monday. She played Prokofiev (8 Pieces from Op 12) and Beethoven (Sonata in E Flat Major, Op.31 No.30). Such technical control combined with joie de vivre and with poetic sensitivity too when called for. Really as good as it gets. The audience loved her as usual, and she responded wreathed in smiles. A delight. You can listen on BBC Sounds for another four weeks.

Core logic again

I have mentioned Neil Tennant’s system(s) of what he calls Core Logic once or twice before on this blog, in friendly terms. For the very shortest of introductions to the core idea of his brand of relevant logic, see my post here on the occasion of the publication of his book on the topic. (And there is a bit more info here in a short note in which I respond to some criticisms on Neil’s behalf — unnecessarily, it turned out, as he published his own rejoinder.)

I notice that Neil has now written a piece outlining his developed ideas on Core Logic for Philosophia Mathematica. If you want to know more, this might be a good place to start. You can download this paper here.

Scroll to Top