I have just read Stephen Budiansky’s Journey to the Edge of Reason: The Life of Kurt Gödel (OUP 2021). And no, I’m not immediately breaking my self-denying resolution to concentrate on finishing the Study Guide — I wanted to know if this biography should get a recommendation in the historical notes of the relevant chapter!

I’ll be brisk. Budiansky’s book comes much praised. But, to be honest, I’m not really sure why. You’ll certainly learn much more about Gödel’s ideas and intellectual circles from John Dawson’s reliable and thoughtful Logical Dilemmas: The Life and Work of Kurt Gödel (A. K. Peters, 1997). When Budiansky occasionally ventures to explain something in Gödel’s work, he too often just gets it wrong. And a lot of the scene-setting background in his book about Brno in 1910s, Vienna in the 1920s and 1930s, Princeton during and after the war, is routine stuff (and a bit too much of it is just padding). For example, the anti-semitism in the Austrian universities in the thirties, the speedy rehabilitation of Nazi collaborators after the war, is still shocking: but there is no depth to the familiar story as recounted here. Yes, the book rattles along and is easily readable. But does it add much to our understanding of things that matter? I certainly don’t feel any better or wiser for knowing a few more of the sad details about Gödel’s later health and fragile mental state. When does biographical curiosity slide into shabby prurience? If you want to read about Gödel’s life, stick to Dawson.

So August was the first full month for Logic Matters with its snappy new web host, and with its sparse new look. Everything seems to have settled down to be working pretty satisfactorily (though some further minor tinkering remains to be done when I am in the mood). The stats are pretty much in line with the previous averages — just under 40K unique visitors in the first month. Or so they say. I’m never sure quite what to read into such absolute numbers.

Relative numbers are more reliable, no doubt. And one consistency is that — month by month — the Study Guide gets downloaded more than the Three Big Red Logic Books combined. So really that settles what I need to do next. Namely, eschew all kinds of logical distractions and concentrate on actually finishing rewriting the damned thing: no more procrastination. So that’s my plan for the next ten weeks. I have a time-table. And, if things don’t go too far adrift, I hope to start posting excerpts from the new version here by the end of the month. Who knows? — I might even get a few useful comments/suggestions from new contributors …

The overall strategy of Gentzen’s consistency proof for PA can be readily described. We map proofs in his sequent calculus version of PA to ordinals less than 𝜀_{0}. We show that there’s an effective reduction procedure which takes any proof in the system which ends with absurdity/the empty sequent and outputs another proof with the same conclusion but a smaller assigned ordinal. So if there is one proof of absurdity in PA, there is an infinite chain of such proofs indexed by an infinite descending chain of ordinals. That’s impossible, so we are done.

The devil is in all the details. And these will depend, of course, on the exact system of PA which we work with. If we do indeed start from something close to Gentzen’s own system, then things quickly get obscurely intricate in a very untransparent way. The assignment of ordinals initially seems pretty ad hoc and the reduction procedure horribly messy. It is the presence of PA’s induction rule which causes much of the trouble. So as Michael Rathjen suggests in his entry on Proof Theory in the Stanford Encyclopedia, it turns out to be notably more elegant to introduce an infinitary version of PA with the omega-rule replacing the induction rule, and then proceed in two stages. First show that we can unfold any PA deduction into a PA𝜔 deduction, and then do a significantly neater Gentzen-style consistency proof for PA𝜔 (the general idea was worked out by Schütte, and is familiar to old hands from the tantalizing fourteen-page Appendix in the first edition of Mendelson’s classic book!).

Mancosu, Galvan and Zach, however, stay old-school, giving us something close to Gentzen’s own proof. Even with various tweaks to smooth over some bumps, after an initial dozen pages saying a bit more about PA, this takes them sixty-five pages. And yes, these pages are spent relentlessly working though all the details for the specific chosen version of PA, with extended illustrations of various reduction steps. It is not that the discussion is padded out by e.g. a philosophical discussion about the warrant for accepting the required amount of ordinal induction; nor are there discussions of variant Gentzen-style proofs like Schütte‘s. Is the resulting hard slog worth it?

A mixed verdict (and I’ll be brief too, despite the length of these chapters — as I don’t think there is much profit in trying to summarise here e.g. the stages of the reduction procedure, or in looking at particular points of exposition). There’s something positive to say in a moment. But first the more critical comment.

It sounds so very very ungrateful, I know, but I didn’t find the level of exposition here that brilliant. The signposting along the way could be more brightly lit (long sections aren’t subdivided, and [mixing my metaphors!] crucial paragraphs can appear without fanfare — see e.g. half way down p. 280). And more importantly, page by page, the exposition could often be at least a couple of degrees more perspicuous. It is not that the proof details here are particularly difficult; but still, and really rather too often, I found myself having to re-read or backtrack, or having to work out the motivation for a technical detail for myself. I predict, then, that many of IPT’s intended readers (who may, recall, “have only a minimal background in mathematics and logic”) will find this less than maximally clear, and — to say the least — markedly tougher going than the authors wanted. The logically naive reader will struggle, surely.

But now forget about IPT’s official mission-statement! On the bright side, the more sophisticated reader — someone with enough mathematical nous to read these chapters pausing over the key ideas and explanations while initially skipping/skimming over much of the detail (and having a feel for which is likely to be which!) — should actually end up with a very good understanding of the general structure of Gentzen’s proof and what it is going to take to elaborate it. Such a reader should find that — judiciously approached — IPT provides a more attractive introduction than e.g. Takeuti’s classic text. So that’s terrific! But as I say, I think this probably requires a reader not to do the hard end-to-end slog, but to be mathematically able and confident enough to first skim through to get the headline ideas, and then do a second pass to get more feel for the shape of some of the details; the reader can then drill down further to work through as much of the remaining nitty-gritty that they then feel that they really want/need (though for many, that is probably not much!). For this more sophisticated reader, prepared to mine IPT for what they need in an intelligent way, these chapters on Gentzen’s consistency proof will indeed be a great resource.

As I said in the last post, Chapter 7 of IPT makes a start on Gentzen’s (third, sequent calculus) proof of the consistency of arithmetic. Chapter 8 fills in enough of the needed background on ordinal induction. Then Chapter 9 completes the consistency proof. I’ll take things in a different order, commenting briefly on the relatively short ordinals chapter in this post, and then tackling the whole consistency proof (covering some 77 pages!) in the next one.

§8.1 introduces well-orders and induction along well-orderings, and §8.2 introduces lexicographical and related well-orderings. Then §§8.3 to 8.5 are a detailed account of ordinal notations for ordinals less than 𝜀_{0}, and carefully explain how these can be well-ordered.

Mancosu, Galvan and Zach rightly make it very clear that we can get this far without taking on board any serious set theoretic commitments. In particular, the ordinal notations are finite syntactic objects and, if o_{1} and o_{2} are two distinct notations, it is decidable by a simple procedure which comes first in the well-ordering. However, §8.6 does pause to present “Set-theoretic definitions of the ordinals”, and the discussion continues in §8.7 and §8.8. These are written as if for someone who knows almost no set theory: but I suspect that they’d go too fast for a reader who hasn’t previously encountered von Neumann’s implementation of the ordinals by sets. (And I’d certainly want to resist our present authors uncritical identification of ordinals with their von Neumann implementations! — ordinals are numbers that can be modelled in set theory in the way that other kinds of numbers can be modelled in set theory, but are not themselves sets. But that’s a battle for another day!)

The chapter finishes with §8.9, where sets drop out of the picture again. We here get a brisk treatment of arguments by ordinal induction up to 𝜀_{0} for the termination of (i) the fight with the Hydra, and (ii) the Goodstein sequence starting from any number. These are lovely familiar examples: the discussion here is OK, but not especially neatly or excitingly done.

Back though to the earlier parts of the chapter, up to and including §8.5. These are pretty clear (though I suppose parts might go a bit quickly for some students). They should do the needed job of giving the reader enough grip on the idea of ordinal induction to be able to understand its use in Gentzen’s consistency proof. Onwards, then, to the main event …!

Let’s pause to take stock. Chapters 3 to 6 of IPT comprise some two hundred pages — a book’s worth in itself — on Gentzen-style natural deduction and normalization theorems, and then on the sequent calculus and cut-elimination theorems. These topics are much-discussed elsewhere, at various levels of sophistication. What’s distinctive about the coverage of IPT is that it is (i) supposed to be accessible to near beginners in logic, while (ii) sticking pretty closely to discussing Gentzen’s own formal systems, and Gentzen’s own proofs about them (and later developments of them): “One of the main goals we set for ourselves,” say the authors, “is that of providing an introduction to proof theory which might serve as a companion to reading the original articles by Gerhard Gentzen.” Moreover, (iii) “In order to make the content accessible to readers without much mathematical background, we carry out the details of proofs in much more detail than is usually done.”

In discussing these four chapters, I’ve quibbled about various points of presentation. But I suppose my main unhappiness has been about the overall shape of the project itself, given the intended readership. Gentzen is often a remarkably clear writer; but I’m not at all convinced that sticking so closely to his original papers is the best way to start learning about structural proof theory. And I’m even less convinced that giving massively detailed proofs is the way to help the beginner get clear about the Big Ideas (especially when so many of the details are pretty tedious, and are made more tedious by the decision to cleave to Gentzen’s original formal systems). Of course, I’m not the intended naive reader, and (unlike the authors!) I haven’t given lecture courses on proof theory: maybe their approach works a treat with many students. All I can do is register my doubts, and (as I have done in passing) suggest familiar alternatives that on balance I would recommend more warmly to beginners, who can then dip into IPT if/when they feel the need.

But now we move on to the last three chapters of the book. These focus on Gentzen’s third proof of the consistency of arithmetic — the one using ordinal induction in the setting of a sequent calculus presentation of arithmetic. Chapter 7 makes a start at setting up the proof. Chapter 8 pauses to explain ordinal notations and the idea of ordinal induction. Then the final Chapter 9 makes use of ordinal induction to complete the consistency proof.

Now, while there are quite a few other options for expositions of natural deduction and sequent calculi available for readers with different levels of mathematical sophistication but little background logic, here the situation is surely quite different. Yes, there are a fair number of very short presentations (a few paragraphs) giving an arm-waving explanation of the basic proof-idea of Gentzen’s second or third proofs: but we don’t have even an handful of worked through but still accessible accounts of how the argument goes. There’s the chapter in Gaisi Takeuti’s justly admired 1975 Proof Theory, but that’s fairly tough going for anyone. I’ve seen the long Chapter 1 of Wolfram Pohler’s 1989 Proof Theory described as giving “a very clean, streamlined approach”, but — to say the very least — it will be impenetrable for the relative beginner. There’s a little 77 page 2014 book by Anna Horská with the promising title Where is the Gödel-Point Hiding: Gentzen’s Consistency Proof of 1936 and his Representation of Constructive Ordinals. It’s dreadful. What else is there?

Paolo Mancosu, Sergio Galvan and Richard Zach therefore have little competition here. Any decent presentation of Gentzen’s argument which makes it more available will be very welcome. And, taking a very superficial look at the next chapter, it seems that you don’t have to have read all the previous chapters in order to join the party here. Assuming you already know a bit about the sequent calculus and cut elimination proofs, my impression is that a quick skim of Chapter 6 will be enough to set you up for diving into Chapter 7. Which is good.

These final chapters are the ones that I’ve been most looking forward to seeing: so how do they work out?

There used to be a little subscription form in the sidepanel of the old-look Logic Matters where you could subscribe to get email notifications whenever there was an update here. I’ve decided against replicating this. Instead of auto-generated mailings, I’ll just send out occasional short Newsletters to alert people to the more interesting new postings or series of postings. Here’s the first Newsletter, as sent out to previous subscribers. If you want to get future such mailings — and I promise your email box will not be cluttered! — then you can subscribe by following this link. (There’s a permanent link in the footer of those pages which have them.)

And it is now exactly a year since the self-published version of the second edition of An Introduction to Formal Logic was published as a paperback. This sells about 75 copies a month, very steadily. Again, the figure strikes me as surprisingly high, given that the PDF has also been freely available all along — and that’s downloaded about 850 times a month. Some of the online support materials, like the answers to exercises, are quite well used too. All in all, pretty pleasing.

I occasionally get friendly feedback about the book: and it will be interesting to see if sales/downloads jump at the beginning of the new term/semester as one or two more lecturers adopt the book as a main text. I do hope so (if only because students shouldn’t be being asked to fork out $100 for second-rate course-texts!).

Still, there’s a lot about this book that could be better, so I really do want to have a third bash at an introductory logic text, and sooner rather than later. But I haven’t yet decided quite how to handle this. Something that is recognisably a third edition of the present book? Or, leaving this version out there as it is (apart from any needed corrections), a rather different, brisker book, requiring just a bit more of the reader? Choices, choices …

We are already two hundred pages into IPT: but onwards! We’ve now arrived at Chapter 6, The Cut-Elimination Theorem. Recall, the sequent calculus that Mancosu, Galvan and Zach have introduced is very much Gentzen’s; and now their proof of cut elimination equally closely follows Gentzen.

The story goes like this. The chapter begins by introducing the mix rule, which is easily seen to be equivalent to the cut rule. Suppose then we can establish the Main Lemma that a classical proof with a single mix as its final step can be transformed into a mix-free proof of the same end-sequent. Repeatedly applying the Main Lemma top-down to subproofs of a given proof and we’ll get a mix-free version: and proving the eliminability of mixes like this is enough to establish the cut-elimination theorem.

So (§6.1) we get some preliminary definitions of the degree and rank of a proof (dependent on the occurrences of mixes), and (§6.2) a strategy for proving the Main Lemma is described — do a double induction on the degree and rank of proofs ending with a single mix. The basic strategy is clearly explained, but working through the proof involves tackling a lot of cases — and our authors insist on laborious completeness “for systematic and pedagogic reasons”. Hence §6.3 to 6.5 then fill out the detailed proof over twenty-nine(!) pages. §6.6 and §6.7 give examples of degree-lowering and rank-lowering transformations in action. §6.8 notes how the proof for the Gentzen’s classical sequent calculus carries over to the intuitionist case. Then §6.9 pauses to explain why the proof-strategy for establishing mix-elimination doesn’t carry over to a direct proof for cut-elimination (that’s good! — I can’t recall offhand other presentations usually doing this as explicitly, other than von Plato’s Handbook piece on ‘Gentzen’s Logic’). Then finally, after fifty pages, we get two sections on consequences of cut-elimination.

Page-by-page, this is mostly pretty clear (perhaps not so much in the proof of the midsquent theorem in §6.11). But we aren’t told what the pedagogic reasons are for doing everything this way, at this level of minute detail. Once the strategy for proving the Main Lemma has been outlined, what will the alert reader gain from hacking through nearly thirty pages of detail as opposed to something like e.g. Takeuti’s six pages of headlines? And tackling Gentzen’s original LK system with sequences rather than multisets either side of the sequent arrow already makes proofs unnecessarily messy. Takeuti wisely makes what really matters in proof transformations vivid by leaving out steps, with placeholders like “some exchanges”: IPT puts in every step so you frequently have to look two or three times to see the crucial moves. Why?

But more basically, why the sole focus on Gentzen’s original sequent calculus when it is well known that revised systems like G3i and G3c lend themselves rather more neatly to cut-elimination proofs? Working with those systems you get to the essence of what’s going on without unnecessary distractions. Historical piety and faithfulness to Gentzen’s original is all very well in its place; but perhaps its place isn’t in shaping a reader’s first encounter with sequent calculi and their proof theory.

To make the obvious comparison, the first four chapters of von Plato and Negri’s Structural Proof Theory cover the basics of the sequent calculus approach, with chapters on intuitionist propositional logic (focusing on the propositional version of G3i), classical propositional logic (cut down from G3c), and then the full first-order versions, with cut-elimination theorems for each case snappily proved along the way (the details are there, but much less painful). There are also discussions of the consequences of cut elimination, and many more asides, all done in a pretty reader-friendly way in twenty-five fewer pages than IPT. What’s not to like?

It is exactly a year ago that the self-published version of An Introduction to Gödel’s Theorems was published as a paperback. It has sold over seven hundred copies in that time, and the monthly trend is slowly upwards. That’s three times as many copies as the CUP paperback was selling. But then, this print-on-demand version is a third of the cost! Even so, the sales figure strikes me as surprisingly high, given that the PDF has also been freely available at the same time as the new paperback. I guess it shows that quite a few people, like me, do prefer to work from a physical book, if one is available at a modest price. As far as downloads go, AWStats currently reports about five hundred a month — though who knows exactly what these (rather volatile) download stats really mean. Still, I count do that as overall a happy success!

Who knows if I will ever get round to a third edition. There’s tidying to be done, and I’d quite like to add a bit more around and about the Second Theorem. It would be fun to catch up with some reading and re-reading and re-thinking. But I don’t cringe when I occasionally have occasion to glance at the book: so I’m not yet feeling an urgent push to getting back to revising it right now.

This chapter is on The Sequent Calculus. We meet Gentzen’s LJ and LK, with the antecedents and succedents taken to be sequences of formulas. It is mentioned that some alternative versions treat the sequent arrow as relating multisets so the corresponding structural rules will be different; but it isn’t mentioned that alternative rules for the logical connectives are often proposed, making for some alternative sequent calculi with nicer formal features. The definite article in the chapter title could mislead.

And how are we to interpret the sequent arrow? Taking the simplest case with a single formula on each side, we are initially told that A ⇒ B “has the meaning of A ⊃ B” (p. 169). But then later we are told that “we might interpret such a sequent [as A ⇒ B] as the statement that B can be deduced from the assumption A” (p. 192, with letters changed). So which does it express? — a material conditional or a deducibility relation? I vote for saying that the sequent calculus is best regarded as a regimented theory of deducibility!

Now, at this point in the book, the conscientious reader of IPT will have just worked through over a hundred pages on natural deduction. So we might perhaps have expected to get next some linking sections explaining how we can see the sequent calculus as in a sense a development from natural deduction systems. I am thinking of the sort of discussion we find in the very helpful opening chapter ‘From Natural Deduction to Sequent Calculus’ of Jan von Plato and Sara Negri’s Structural Proof Theory (CUP, 2001). But as it is, IPT dives straight, presenting LK. There is, by the way, zero discussion here or later why the rules of LK have the particular shape they have (namely, to set up the single-succedent version as the intuitionist calculus).

IPT then immediately starts considering proof discovery by working back from the desired conclusion, with the attendant complications that arise from using sequences rather than sets or multisets. This messiness at the outset doesn’t seem well calculated to get a student to appreciate the beauty of the sequent calculus! I wouldn’t have started quite like this. However, the discussion here does give some plausibility to the claim that provable sequents should be provable without cut.

A proof of cut elimination will be the topic of the next chapter. The rest of this present chapter goes through some more sequent proofs, and proves a couple of lemmas (e.g. one about variable replacement preserving proof correctness). And then there are ten laborious pages showing how an intuitionist natural deduction NJ proof can be systematically transformed into an LJ sequent proof, and vice versa — just giving outline proofs would have done more to promote understanding.

The lack of much motivational chat at the beginning of the chapter combined with these extended and less-than-thrilling proofs at the end do, to my mind, make this a rather unbalanced menu for the beginner meeting the sequent calculus for the first time. At the moment, therefore, I suspect that many such readers will get more out of, and more enjoy, making a start on von Plato and Negri’s book. But does IPT’s Chapter 6 on cut elimination even up the score?