The chapter on model theory in the Beginning Mathematical Logic Study Guide was last updated quite recently, in particular to take account of Roman Kossak’s nice 20221 book Model Theory for Beginners (College Publications). Rather little has changed, then, in this current revision, except some minor tidying (though I have dropped as unnecessary a previously footnoted long proof). But still, here it is, the revised Chapter 5 (as it is now numbered).
I have only just noticed that a recording of Elisabeth Brauß playing the four Schubert Impromptus D.899 last year is available now and for another week on BBC Sounds (start at 10 minutes into the programme).
This strikes me as extraordinarily good and very moving — with so much thought gone into every bar, yet the playing utterly honest and direct and unmannered. I have more than a dozen wonderful recordings of the impromptus from Schnabel on; but these performances bear comparison (in that these too are such that, while you listen, you can’t help but feel “yes, this is how the Schubert should be played …”).
Judging from her Mozart and Beethoven too, one day — and I do hope that this is where her inclinations take her! — Elisabeth Brauß could become one of the very finest of Schubert pianists. And, with the clock ticking away, I hope I will still be here to hear her.
What to cover in the Guide straight after standard classical FOL?
Theories expressed in first-order languages with a first-order logic turn out to have their limitations — that’s a theme that will recur when we look at model theory, theories of arithmetic, and set theory. You will find explicit contrasts being drawn with richer theories expressed in second-order languages with a second-order logic. That’s why — although this is of course a judgement call — I do on balance think it is worth knowing just something early on about second-order logic, in order to be in a position to understand something of the contrasts being drawn. Hence this next short chapter.
There are no very substantive changes from the previous version. But it is a little tidier in some respects. So here is Chapter 4: Second-order logic, quite briefly.
Here is the first main chapter of the Study Guide, on First-Order Logic. Nothing much has changed in the recommendations (or the occasional disparaging comments about non-recommended books!). However, the surrounding chat has been tidied up. I have in particular heeded a friendly warning about “mission creep” (the overview sections were getting too long, too detailed — especially about various proof-systems). So I hope the balance is improved.
One comment (which I have also now added to Chapter 1 — the section on “Choices, choices” where I say something about how I have decided which texts to recommend). If I were choosing a text book around which to shape a lecture course on FOL, or some other topic, I would no doubt be looking at many of the same books that I mention in the Guide; but my preference-rankings could well be rather different. So, to emphasize, the recommendations in this Guide are for books which I think should be particularly good for self-studying logic, without the benefit of classroom introductions or backup.
As I’ve mentioned before, I have started work on revising/updating/extending/cutting-down the much-used Study Guide (Teach Yourself Logic as was, now retitled a bit more helpfully Beginning Mathematical Logic).
I’d thought about dropping the three-part structure. But I have decided, after some experimentation, to keep it. So after some preliminaries, Part I is on the core math logic curriculum. Part II (fairly short) looks sideways at some ways of deviating from/extending standard FOL. Part III follows up the topics of Part I at a more advanced level. So, for example, there is an introductory chapter on e.g. model theory in Part I, and then some suggestions about more advanced reading on model theory in another chapter in Part III. (Having one long chapter on model theory, one long chapter on arithmetic, etc. made for unwieldy and dauntingly long chapters, so that’s why it is back to the original plan.)
Over the next couple of weeks, I’ll be posting some early revised chapters from Part I, and I’ll very much be welcoming comments and suggestions (and corrections, of course) at this stage. Please, please, don’t hesitate to have your say (either using the comments boxes, or by email to peter_smith at logicmatters.net). A lot of students — possibly including your own students! — are downloading the Guide each month: if you think they are being led astray, now is the time to say!
Here then, for starters, are the Preface and a couple of preliminary chapters. Not terribly exciting, but much snappier than before. They will explain more about the structure and coverage of the Guide to those who don’t already know it. Next up, the long key chapter on FOL.
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 very 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 much 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; they can then drill down further again 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.
And on that happier note, let me end!
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 o1 and o2 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 …!
To be continued
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?
To be continued