The revised Study Guide — elementary proof theory

Here is the draft final chapter of Part I of Beginning Mathematical Logic — so this is the last of the group of chapters on core topics at an elementary level. This one on proof theory is newly written; comments will therefore be particularly welcome.

Having got this far, I am well aware that there are now some mismatches in the level/breadth of the overviews in the various chapters, and also places which call for more cross-references.  For example, I need to go back to the overview on set theory to say just a paragraph or so more about ordinals, in order to make a better connection with the use of small ordinals in the current chapter when waving my arms at Gentzen’s consistency proof. So smoothing out the coverage of Part I of the Study Guide is a next task. But at least there is now a full draft to play with.

The revised Study Guide — intuitionistic logic

After the minor revisions of earlier chapters of the Beginning Mathematical Logic Study Guide, something more exciting! Here is a brand new chapter on intuitionistic logic.

The chapter starts by briskly outlining a standard natural deduction system for intuitionistic logic. Then there are two sections giving rough-and-ready overviews, one on motivation and the BHK interpretation, the other on some additional formal details and giving a sketch of Kripke semantics. There are then the usual sections suggesting main readings, followed by some additional reading options. The chapter ends with some pointers to a few pieces with a more historical/philosophical flavour. The usual chapter format, in other words.

Since this is newly minted, I’d very much welcome comments/suggestions — particularly about alternative/additional readings at the right kind of introductory level. (Also very welcome, advance suggestions for what should appear in the planned later section when we briefly revisit intuitionism at a more sophisticated level in Part III of the Guide.)

And in Big Red Logic Book news …

Brief version: There is now a hardback version available of the second edition of An Introduction to Formal Logic: ISBN 978-1916906327. It should now be available to order from bookshops (as well as from Am*z*n and some other online sellers). It is priced at £20/$25, about the minimum possible. I’ve just got a sample copy and it is very decently produced.

Longer version: You’ll probably recall that I recovered the copyright of the second edition of IFL a year ago so that I could make the PDF freely available (a pretty small gesture in these difficult times, but every little helps). Lots of students, though, do prefer to work from a physical book: so I also set up an inexpensive print-on-demand paperback (to minimise the cost, that is Am*z*n only). 

Now, as I’ve said before, self-publishing has the downside that the word doesn’t get out to librarians via a publisher’s fancy catalogue. But in any case, in last year’s lockdown, and more recently too, librarians were rightly concentrating on improving their e-resources, so it didn’t seem the time to fuss too much about getting physical copies into libraries. However, things are slowly returning to something more like the old normality for library operations. So I have now arranged for ‘proper’ hardback copies — printed by Lightning Source who do small-run/on-demand printing for some academic presses — to be available for library purchase at minimum cost from, inter alia, standard library suppliers. So do please ask your friendly local university or college librarian to order a copy or two (emphasizing, if you need to, that this is a significantly changed book from the first edition). Online resources are all well and good, though problematic for some students: to repeat, at textbook-length, many — like me — do much prefer to have real books available!

The revised Study Guide — model theory

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).

The revised Study Guide — second-order logic

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.

The revised Study Guide — first-order logic

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.

The revised Study Guide — preliminary instalment

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.

Back to the Study Guide …

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 …

An Introduction to Proof Theory, Ch. 7 and Ch. 9

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.

And on that happier note, let me end!

An Introduction to Proof Theory, Ch. 8

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

Scroll to Top