Avigad’s MLC — First order logic

Last year I wrote a number of posts on Jeremy Avigad’s major recent book for advanced students, Mathematical Logic and Computation (CUP, 2022). I was reading it with an eye to seeing what parts might be recommended in the next iteration of the Study Guide. This is a significantly shorter version combining the posts, now removed, on the first part of the book. A brisker post on the rest of the book will follow.

The first seven chapters of MLC, some 190 pages, form a book within the book, on core FOL topics but with an unusually and distinctively proof-theoretic flavour. This is well worth having. But a reader who is going to happily navigate and appreciate the treatments of topics here will typically need significantly more background in logic than Avigad implies. The exposition is often very brisk, and the amount of motivational chat is variable and sometimes minimal. So — to jump to the verdict — some parts of this book will indeed be recommended in the Guide, but as supplementary reading for those who have already tackled one of the standard FOL texts.

To get down to details …

Logical Methods — on modal logic

Moving on through Greg Restall and Shawn Sandefer’s Logical Methods, Part II is on propositional modal logic. So the reader gets to find out e.g. about S4 vs S5 and even hears about actuality operators etc. before ever meeting a quantifier. Not an ordering that many teachers of logic will want to be following. But then, as I have already indicated when discussing Part I on propositional logic, I’m not sure this is really working as the first introduction to logic that it is proclaimed to be (“requires no background in logic”). I won’t bang on about that again. So let’s take Part II as a more or less stand-alone treatment that could perhaps be used for a module on modal logic for philosophers, for those who have already done enough logic. What does it cover? How well does it work?

Part I, recall, takes a proof-theory-first approach; Part II sensibly reverses the order of business. So Chapter 7 on ‘Necessity and Possibility’ is a speedy tour of the Kripke semantics of S5, then S4, then intuitionistic logic. I can’t to be honest say that the initial presentation of S5 semantics is super-clearly done, and the ensuing description of what are in effect unsigned tableaux for systematically searching for counterexamples to S5 validity surely is too brisk (read Graham Priest’s wonderful text on non-classical logics instead). And jumping to the other end of the chapter, there is a significant leap in difficulty (albeit accompanied by a “warning”) when giving proofs of the soundness and completeness of initutionistic logic with respect to Kripke semantics. Rather too much is packed in here to work well, I suspect.

Chapter 8 is a shorter chapter on ‘Actuality and 2D Logic’. Interesting, though again speedy. But for me, the issue arises of whether — if I were giving a course on modal logic for philosophers — I’d want to spend any time on these topics as opposed to touching on the surely more interesting philosophical issues generated by quantified modal logics.

Chapter 9 gives Gentzen-style natural deduction systems for S4 and S5. Which is all technically fine, of course. But I do wonder about how ‘natural’ Gentzen proofs are here, compared with modal logic done Fitch-style. I certainly found the latter easier to motivate in class. So Gentzen-style modal proof systems would not be my go-to choice for a deductive system to introduce to philosophy student. Obviously Restall and Sandefer differ!

Overall, then, I don’t think the presentations will trump the current suggested introductory readings on modal logic in the Study Guide.

Restall & Standefer, Logical Methods

A new introductory logic textbook has just arrived, Greg Restall and Shawn Standefer’s Logical Methods (MIT).

This promises to be an intriguing read. It is announced as “a rigorous but accessible introduction to philosophical logic” — though, perhaps more accurately,  it could be said to be an introduction to some aspects of formal logic that are of particular philosophical interest.

The balance of the book is unusual. The first 113 pages are on propositional logic. There follow 70 pages on (propositional) modal logic — this, no doubt, because of its philosophical interest. Then there are just 44 pages on standard predicate logic, with the book ending with a short coda on quantified modal logic. To be honest, I can’t imagine too many agreeing that this reflects the balance they want in a first logic course.

Proofs are done in Gentzen natural deduction style, and proof-theoretic notions are highlighted early: so we meet e.g. ideas about reduction steps for eliminating detours as early as p. 22, so we hear about normalizing proofs before we get to encounter valuations and truth tables. Another choice that not everyone will want to follow.

However, let’s go with the flow and work with the general approach. Then, on a first browse-and-random-dipping, it does look (as you’d predict) that this is written very attractively, philosophically alert and enviably clear. So I really look forward to reading at least parts of Logical Methods more carefully soon. I’m turning over in my mind ideas for a third edition of IFL and it is always interesting and thought-provoking to see how good authors handle their introductory texts.

Self-publishing and the Big Red Logic Books

One way of increasing the chance of your books actually being read is to make them freely downloadable in some format, while offering inexpensive print-on-demand paperback versions for those who want them. Or at least, that’s a publication model which has worked rather well for me in the last couple of years. Here’s a short report of how things went during 2022, and then just a few general reflections which might (or might not) encourage one or two others to adopt the same model!

As I always say, the absolute download stats are very difficult to interpret, because if you open a PDF in your browser on different days, I assume that this counts as a new download — and I can’t begin to guess the typical number of downloads per individual reader (how many students download-and-save, how many keep revisiting the download page? who knows?). But here is the headline news:

PDF downloadsPaperback sales
Intro Formal Logic112211112
Intro Gödel’s Theorems7432627
Gödel Without Tears4394677
Beginning Mathematical Logic25863493

No doubt, the relative download figures, comparing books and comparing months, are more significant: and these have remained very stable over the year, with about a 10% increase over the previous year.

As for paperback sales of the first three books, these too remain very steady month-by-month, and the figures are very acceptable. So we have proof-of-concept: even if a text is made freely available, enough people prefer to work from a printed text to make it well worthwhile setting up an inexpensively priced paperback. (In addition there’s also a hardback of IFL which sold 150 copies over the year, and a hardback of the first edition of GWT sold 40 copies up to end of October, before being replaced by a new hardback edition.)

The BML Study Guide was newly paperbacked at the beginning of the year, not with any real expectation of significant sales given the rather particular nature of the book. Surprisingly, it is well on course to sell over 500 copies by its first anniversary.

Obviously, an author wants their books to conquer the world — why isn’t just everyone using IFL? —  but actually, I’m pretty content with these statistics.

To repeat what I said when giving an end-of-year report at the beginning of last January, I don’t know what general morals can be drawn from my experiences with these four books. Every book is what it is and not another book, and every author’s situation is what it is.

But providing an open-access PDF plus a very inexpensive but reasonably well produced paperback is obviously a fairly ideal publication model for getting stuff out there. I’d be delighted, and — much more importantly — potential readers will be delighted, if rather more people followed the model.

Yes, to produce a book this way, you need to be able to replicate in-house some of the services provided e.g. by a university press. But volunteer readers — friends, colleagues and students — giving comments and helping you to spot typos will (if there is a reasonable handful of them) probably do at least as good a job as paid publisher’s readers, in my experience. Writers of logic-related books, at any rate, should be familiar enough with LaTeX to be able to do a decent typographical job (various presses make their LaTeX templates freely available — you can start from one of those if you don’t feel like wrangling with the memoir class to design a book from scratch). Setting up Amazon print-on-demand is a doddle. You’ll need somehow to do your own publicity. But none of these should be beyond the wit of most of us!

The major downside of do-it-yourself publishing, of course, is that you don’t get the very significant reputational brownie points that accrue from publication by a good university press. And we can’t get away from it: job-prospects and promotions can turn on such things. So they will matter a great deal in early or mid career.

But for those who are well established and nearer the end of their careers, or for the idle retired among us … well, you might well pause to wonder a moment about the point of publishing a monograph with OUP or CUP (say) for £80, when you could spread the word to very many more readers by self-publishing. It seems even more pointless to publish a student-orientated book of one kind or another at an unaffordable price. So I can only warmly encourage you to explore the do-it-yourself route. (I’m always happy to respond to e-mailed queries about the process.)

Finally, I can somewhat shamefacedly add a last row to the table above, about work in (stuttering) progress towards an announced but as yet far from finished paperback:

PDF downloadsPaperback sales
Beginning Category Theory7482N/A

This download figure is embarrassing because, as I’ve said before, I know full well these notes are in a really rackety state. But I can’t bring myself to abandon them. So my logical New Year’s resolution is to spend the first six weeks of the year getting at least Part I of these notes (about what happens inside categories) into a much better shape. I just need to really settle at last to the task and not allow myself so many distractions. Promises, promises. Watch this space.

Avigad MLC — 6: Arithmetics

Chs 1 to 7 of MLC, as we’ve seen, give us a high-level and often challenging introduction to core first-order logic with a quite strongly proof-theoretic flavour. Now moving on, the next three chapters are on arithmetics — Ch. 8 is on primitive recursion, Ch. 9 on PRA, and Ch. 10 on richer first-order arithmetics.

I won’t pause long over Ch. 8, as the basic facts about p.r. functions aren’t wonderfully exciting! Avigad dives straight into the general definition of p.r. functions, and then it’s shown that the familiar recursive definitions of addition, exponentiation, and lots more, fit the bill. We then see how to handle finite sets and sequences in a p.r. way. §8.4 discusses other recursion principles which keep us within the set of p.r. functions, and §8.5 discusses recursion along well-founded relations — these two sections are tersely abstract, and it would surely have been good to have more by way of motivating examples. Finally §8.6 tells us about diagonalizing out of the p.r. functions to get a computable but not primitive recursive function, and says just a little about fast-growing functions. All this is technically fine, it goes without saying; though once again I suspect that many students will find this chapter more useful if they have had a preliminary warm-up with a gentler first introduction to the topic first.

But while Ch. 8 might be said to be relatively routine (albeit quite forgiveably so!), Ch. 9 is anything but. It is the most detailed and helpful treatment of Primitive Recursive Arithmetic that I know.

Avigad first presents an axiomatization of PRA in the context of a classical quantifier-free first-order logic. Hence

  1. The logic has the propositional connectives, axioms for equality, plus a substitution rule (wffs with variables are treated as if universally quantified, so from A(x) we can infer A(t) for any term).
  2. We then have a symbol for each p.r. function — and we can think of these added iteratively, so as each new p.r. function is defined by composition or primitive recursion from existing functions, a symbol for the new function is introduced along with its appropriate defining quantifier-free equations in terms of already-defined functions.  
  3. We also have a quantifer-free induction rule: from A(0) and A(x) \to A(Sx), infer A(t) for any term.

§§9.1–9.3 explore this version of PRA in some detail, deriving a lot of arithmetic, showing e.g. that PRA proves that if p is prime, and p \mid xy then either p \mid x or p \mid y, and noting along the way that we could have used an intuitionistic version of the logic without changing what’s provable.

Then the next two sections very usefully discuss two variant presentations of PRA. §9.4 enriches the language and the logic by allowing quantifiers, though induction is still just for quantifier-free formulas. It is proved that this is conservative over quantifier-free PRA for quantifier-free sentences. And there’s a stronger result. Suppose full first-order PRA proves the \Pi_2 sentence \forall x \exists y A(x, y), then for some p.r. function symbol f, quantifier-free PRA proves A(x, f(x)) (and we can generalize to more complex \Pi_2 sentences).

By contrast §9.5 weakens the language and the logic by removing the connectives, so all we are left with are equations, and we replace the induction rule by a rule which in effect says that functions satisfying the same p.r. definition are everywhere equal. This takes us back — as Avigad nicely notes — to the version of PRA presented in Goodstein’s (now unread?) 1957 classic  Recursive Number Theory, which old hands might recall is subtitled  ‘A Development of Recursive Arithmetic in a Logic-Free Equation Calculus’.

All this is done in an exemplary way, I think. Perhaps Avigad is conscious that in this chapter he is travelling over ground that it is significantly less well-trodden in other textbooks, and so here he allows himself to be rather more expansive in his motivating explanations, which works well.

The following Ch. 10 is the longest in the book, some forty two pages on ‘First-Order Arithmetic’. Or rather, the chapter is on arithmetics, plural — for as well as the expected treatment of first-order Peano Arithmetic, with nods to Heyting Arithmetic,  there is also a perhaps surprising amount here about subsystems of classical PA.

In more detail, §10.1 briefly introduces PA and HA. You might expect next to get a section explaining how PA (with rather its minimal vocabulary) can be in fact seen as extending the PRA which we’ve just met (with all its built-in p.r. functions). But we have to wait until  §10.4 to get the story about how to define p.r. functions using some version of the beta-function trick. In between, there are two longish sections on the arithmetical hierarchy of wffs, and on subsystems of PA with induction restricted to some level of the hierarchy. Then §10.5 shows e.g. how truth for \Sigma_n sentences can be defined in a \Sigma_n way, and shows e.g. that I\Sigma_{n+1} (arithmetic with induction for \Sigma_{n + 1} wffs) can prove the consistency of I\Sigma_{n}, and also — again using truth-predicates — it is shown e.g. that I\Sigma_{n} is finitely axiomatizable. (There’s a minor glitch. In the proof of 10.3.5 there is a reference to the eighth axiom of Q — but Robinson arithmetic isn’t in fact introduced until Chapter 12.)

The material here is all stuff that is very good to know. Your won’t be surprised by this stage to hear that the discussion is a bit dense in places; but up to this point it should all be pretty manageable because the ideas are, after all, straightforward enough.

However, the chapter ends with another ten pages whose role in the book I’m not at all so sure about. §10.6 proves three theorems using cut elimination arguments, namely (1) that I\Sigma_{1} is conservative over PRA for \Pi_2 formulas; (2) Parikh’s Theorem, (3) that so-called B\Sigma_{n+1} is conservative over I\Sigma_{n} for \Pi_{n+2} wffs. What gives these results, in particular the third, enough interest to labour through them? They are, as far as I can see, never referred to again in later chapters of the book. And yet §10.7 then proves the same theorems again using model theoretic arguments. I suppose that these pages give us samples of the kinds of conservation results we can achieve and some methods for proving them. But I’m not myself convinced they really deserve this kind of substantial treatment in a book at this level.

Book note: Topology, A Categorical Approach

Having recently been critical of not a few books here(!), let me mention a rather good one for a change. I’ve had on my desk for a while a copy of Topology: A Categorical Approach by Tai-Danae Bradley, Tyler Bryson and John Terilla (MIT 2020). But I have only just got round to reading it, making a first pass through with considerable enjoyment and enlightenment.

The cover says that the book “reintroduces basic point-set topology from a more modern, categorical perspective”, and that frank “reintroduces” rather matters: a reader who hasn’t already encountered at least some elementary topology would have a pretty hard time seeing what is going on. But actually I’d say more. A reader who is innocent of entry-level category theory will surely have quite a hard time too. For example, in the chapter of ‘Prelminaries’ we get from the definition of a category on p. 3 to the Yoneda Lemma on p. 12! To be sure, the usual definitions we need are laid out clearly enough in between; but I do suspect that no one for whom all these ideas are genuinely new is going to get much real understanding from so rushed an introduction.

But now take, however, a reader who already knows a bit of topology and who has read Awodey’s Category Theory (for example). Then they should find this book very illuminating — both deepening their understanding of topology but also rounding out their perhaps rather abstract view of category theory by providing a generous helping of illustrations of categorial ideas doing real work (particularly in the last three chapters). Moreover, this is all attractively written, very nicely organized, and (not least!) pleasingly short at under 150 pages before the end matter.

In short, then: warmly recommended. And all credit too to the authors and to MIT Press for making the book available open-access. So I need say no more here: take a look for yourself!

The Annotated Gödel

Some years ago, Charles Petzold published his The Annotated Turing which, as its subtitle tells us, provides a guided tour through Alan Turing’s epoch-making 1936 paper. I was prompted at the time to wonder about putting together a similar book, with an English version of Gödel’s 1931 paper interspersed with explanatory comments and asides. But I thought I foresaw too many problems. For a start, not having any German, I’d have had to use one of the existing translations, which would lead to copyright issues, and presumably extra problems if I wanted to depart from the adopted translation by e.g. rendering Bew by Prov, etc. And then I felt it wouldn’t be at all easy to find a happy level at which to pitch the commentary.

Plan (A) would be to follow Petzold, who is very expansive and wide ranging about Turing’s life and times, and is aiming for a fairly wide readership too (his book is over 370 pages long). I wasn’t much tempted to try to emulate that.

Plan (B) would be write for a much narrower audience, readers who are already familiar with some standard modern textbook treatment of Gödelian incompleteness and who want to find out how, by comparison, the original 1931 paper did things. You then wouldn’t need to spend time explaining e.g. the very ideas of primitive recursive functions or Gödel numberings, but could rapidly get down to note the quirks in the original paper, giving a helping hand to the logically ept so that they can navigate through. However, the Introductory Note to the paper in the Collected Works pretty much does that job. OK, you could say a bit more (25 pages, perhaps rather than 14). But actually the original paper is more than clear enough for that to be hardly necessary, if you have already tackled a good modern treatment and then read that Introductory Note for guidance in reading Gödel himself.

Plan (C) would take a middle course. Not ranging very widely, sticking close to Gödel’s text. But also not assuming much logical background or any prior acquaintance with the incompleteness theorems, so having to slow down to explain ideas of formal systems, primitive recursion and so on and so forth. But to be frank, I didn’t and don’t think Gödel’s original paper is the best peg on which to hang a first introduction to the incompleteness theorems. Better to write a book like GWT! So eventually I did just that, and dropped any thought of doing for Gödel something like Petzold’s job on Turing.

But now, someone has bravely taken on that project. Hal Prince, a retired software engineer, has written The Annotated Gödel, a sensibly-sized book of some a hundred and eighty pages, self-published on Amazon. Prince has retranslated the incompleteness paper in a somewhat more relaxed style than the version in the Collected Works, interleaving commentary intended for those with relatively little prior exposure to logic. So he has adopted plan (C). And the thing to say immediately — before your heart sinks, thinking of the dire quality of some amateur writings on Gödel — is that the book does look entirely respectable!

Actually, I shouldn’t have put it quite like that, because I do have my reservations about the typographical look of the book. Portions of different lengths of a translation from the 1931 paper are set in pale grey panels, separated by episodes of commentary. And Prince has taken the decidedly odd decision not to allow the grey textboxes containing the translation to split themselves over pages. This means that an episode of commentary can often finish halfway down the page, leaving blank inches before the translation continues in a box at the top of the next page. And there are other typographical choices while also unfortunately make for a somewhat  unprofessional look. That’s a real pity, and does give a quite misleading impression of the quality of the book.

Now, I haven’t read the book with a beady eye from cover to cover; but the translation of the prose seems quite acceptable to me. Sometimes Prince seems to stick a bit closer to the Gödel’s original German than the version in the Works, sometimes it is the other way about. For example, in the first paragraph of Gödel’s §2, we have

G, undefinierten Grundbegriff: W, primitive notion: P, undefined basic notion,

while in the very next sentence we have

G, Die Grundzeichen: W, The primitive signs: P, The symbols.

But such differences are relatively minor.

Where P’s translation of G departs most is not in rendering the German prose but in handling symbolism. W just repeats on the Englished pages exactly the symbolism that is in the reprint of G on the opposite page. But where G and W both e.g. have “Bew(x)”, P has “isProv(x)”. There’s a double change then. First, P has rendered the original “Bew”, which abbreviated “beweisbare Formel”, to match his translation for the latter, i.e. “provable formula”. Perhaps a good move. But Prince has also included an “is” (to indicate that what we have here is an expression attributing a property, not a function expression). To my mind, this makes for a bit of unnecessary clutter here and elsewhere: you don’t need to be explicitly reminded on every use that e.g. “Prov” expresses a property, not a function.

Elsewhere the renditions of symbolism depart further. For example, G has “A_1\mbox{-}Ax(x)” for the wff which says that x is an instance of Axiom Schema II.1. P has “isAxIIPt1(x)”. And there’s a lot more of this sort of thing which makes for some very unwieldy symbolic expressions that I don’t find particularly readable.

There are other debatable symbolic choices too. P has “\Rightarrow” for the object language conditional, which is an unfortunate and unnecessary change. And P writes “x[v \leftarrow y]” for the result of substituting y for v where v is free in x. This may be a compsci notation, but to my untutored eyes makes for mess (and I’d say bad policy too to have arrows in different directions meaning such different things).

Other choices for rendering symbolism involve more significant departures from G’s original but are also arguably happier (let’s not pause to wonder what counts as faithful enough translation!). For example, there is a moment when G has the mysterious “p = 17 Gen q”: P writes instead “p = forall(\mathbf{x_1}, q)”. In G, 17 is the Gödel number for the variable x_1: P uses a convention of bolding a variable to give its Gödel number, which is tolerably neat.

There’s more to be said, but I think your overall verdict on the translation element of Prince’s book might go either way. The prose is as far as I can judge handled well. The symbolism is tinkered with in a way which makes it potentially clearer on the small scale, but makes for some off-putting longwindedness when rendering long formulas. If you are going to depart from Gödel’s symbolism, I don’t think that P chooses the best options. But as they say, you pays your money and makes your choice.

But what about the bulk of the book, the commentary and explanations interspersed with the translation of Gödel’s original? My first impression is definitely positive (as I said, I haven’t yet done a close reading of the whole). We do get a lot of helpful framing of the kind e.g. “Gödel is next going to define … It is easier to understand these definitions if we think about what he needs and where he is going.” And Prince’s discussions as we go along do strike me as consistently sensible and accurate enough, and will indeed be helpful to those who bring the right amount to the party.

I put it like that because, although I think the book is intended for those with little background in logic, I really do wonder whether e.g. the twenty pages on the proof of Gödel’s key Theorem VI will gel with those who haven’t previously encountered an exposition of the main ideas in one of the standard textbooks. This is the very difficulty I foresaw in pursuing plan (C). Most readers without much background will be better off reading a modern textbook.

But, on the other hand, for those who have already read GWT (to pick an example at random!), i.e. those who already know something of Gödelian incompleteness, they should find this a useful companion if they want to delve into the original 1931 paper. Though some of the exposition will now probably be unnecessarily laboured for them, while they would have welcomed some more  “compare and contrast” explanations bringing out more explicitly how Gödel’s original relates to standard modern presentations.

In short, then: if someone with a bit of background does want to study Gödel’s original paper, whereas previously I’d just say ‘read the paper together with its Introductory Note in the Collected Works’, I’d now add ‘and, while still doing that, and depending quite where you are coming from and where you stumble, you might very well find some or even all of the commentary in Hal Prince’s The Annotated Gödel a pretty helpful accompaniment’.

In praise of Truss …

Praise not for our new Prime Minister, about whom the less said the better, but for her admirable logician father John Truss.

By chance, I had occasion recently to dip into his 1997 book Foundations of Mathematical Analysis (OUP) which I didn’t know before and which is excellent. It is my sort of book, in that there is a lot of focus on conceptual motivation and Big Ideas, and a relatively light hand with detailed proofs. E.g. if you want just a very few pages on Gödelian incompleteness, his treatment in the first chapter is exemplary. Or jumping to the end of the book, there is e.g. a really helpful broad-brush section on the ingredients of Gödel’s and Cohen’s independence proofs in set theory, and a very good chapter on constructive analysis and choice principles. In between, we get a story that takes us from the naturals to the integers to the reals to metric spaces and more (e.g. a nice chapter on measure and Baire category). OK, this is a tale which is often told, but I think John Truss’s version is particularly insightful and good at bringing out the conceptual shape of the developing story. So, recommended!

OUP have disappointingly let the book go out of print. A Djvu file can, however, be found at your favourite file depository.

(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.]

One True Logic

There’s a new book out by Owen Griffiths and Alex Paseau, One True Logic: A Monist Manifesto (OUP). As the title suggests, this argues against logical pluralism. Yes, of course, there are myriad logical systems which we can concoct and study as interesting mathematical objects. But what about the logic we actually use in reasoning about them and about other mathematical matters? Is there in fact one correct logic which tracks what really does follow from what? Our authors take a conservative line, in that they are anti-pluralist: there is indeed one true logic for in-earnest applications. They are unconservative in defending a highly infinitary logic in that role.

I’ve read the first few chapters with enjoyment and enlightenment. But I’m going to have to shelve the book for the moment, as it will be too distracting from other commitments to engage seriously with the rest of it for a while. One of the delights of somewhat senior years is finding it more difficult to think about more than one thing at a time. (“But what’s new?” murmurs Mrs Logic Matters from the wings.)

For a start, I must continue cracking on with the category theory project. I have now revised Chapters 1 to 15 of Beginning Category Theory. So here they are, in one long PDF which also includes the remaining unrevised chapters from the 2015/2018 Gentle Intro.

In this iteration there are quite a few minor changes to Chapters 1 to 13 (correcting typos, clarifying some phrasing, deleting an unnecessary section, adding a new theorem in §12.2, etc.), though there is nothing very significant there. I have also now revised Chapter 15, the first of the two general chapters on limits/colimits. This and the preceding chapter on equalisers/co-equalisers could surely do with more polishing and lightening-up in places. But as I’ve said previously, I’m including revised chapters when they are at least an improvement on what went before (I’m not waiting for final-draft perfection!).

If you are like me, you are looking for the more-than-occasional consoling distractions from the state of the wider world. Let me share one.

Of the great pianists I have had the chance to hear live over the years, the one I perhaps find the most emotionally engaging of all is Maria João Pires. Her unmannered directedness goes straight to the heart. So here she is, playing Schubert, Debussy and Beethoven, in a video recorded in Gstaad last August.

Scroll to Top