IPT

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 𝜀₀. 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!

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 𝜀₀, 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₁ and o₂ 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 𝜀₀ 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

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?

To be continued

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?

To be continued

What are we to make of Chapter 4: Normal Deductions? This gives very detailed proofs of normalization, first for the ∧⊃¬∀ fragment of natural deduction, then for the intuitionist system, then for full classical natural deduction, with equally detailed proofs of the subformula property along the way. It all takes sixty-seven(!!) pages, often numbingly dense. You wouldn’t thank me for trying to summarize the different stages, though I think things go along fairly conventional lines. I’ll just raise the question of who will really appreciate this kind of very extended treament?

It certainly is possible to introduce this material without mind-blowing tedium. For example, Jan von Plato’s very readable book Elements of Logical Reasoning (CUP 2013) gets across a rich helping of proof theoretic ideas at a reasonably introductory level with some zest, and has a rather nice balance between explanations of general motivations and proof-strategies on the one hand and proof-details on the other. An interested philosophy student with little background in logic who works through the book should come away with a decent initial sense of its topics, and will be able to appreciate e.g. Prawitz’s Natural Deduction. the more mathematical will then be in a position to tackle e.g. Troesltra and Schwichtenberg’s classic with some conceptual appreciation.

Mancosu, Galvan and Zach’s methodical coverage of normalization isn’t, I suppose, much harder than von Plato’s presentation (scattered sections of which appear at different stages of his book); it should therefore be accessible to those who have the patience to plod though the details of their Chapter 4 and who try not to lose sight of the wood for the trees. But I do wonder whether the slow grind here will really produce more understanding of the proof-ideas. I guess that I can recommend the chapter as a helpful supplement for someone who wants to chase up particular details (e.g. because they found some other, snappier, outline of normalization proofs hard to follow on some point). Is it, however, the best place for most readers to make a first start on the topic? A judgement call, perhaps, but I have to say that I really very much doubt it.

To be continued

Chapter 3 of IPT is on Natural Deduction. The main proof-theoretic work, on normalization, is the topic of the following chapter, and so the topics covered here are relatively elementary ones.

In particular, the first four sections of the chapter simply introduce Gentzen-style proof systems for minimal, intuitionist, and classical logic. So, as with most of the previous chapter, the main question about these sections is: just how good is the exposition?

One initial point. The book, recall, is aimed particularly at philosophy students with only a minimal background in mathematics and logic. But if they are reading this book at all, then — a pound to a penny — they will have done some introductory logic course. And it is quite likely that in this course they will already have met natural deduction done Fitch-style (indenting subproofs in the way expounded in no less than thirty different logic texts aimed at philosophers). It seems strange, to say the least, not to mention Fitch-style natural deduction at all; wouldn’t it have helped many readers to do a compare-and-contrast, explaining why (for proof-theoretic work) Gentzen-style tree layouts are customarily the standard?

An explicit comparison might, indeed, have helped in various places. For example, on p. 73 we are bluntly told that the inference from A to (B ⊃ A) is allowed by the conditional proof rule, i.e. vacuous discharge is allowed. No explanation is given to the neophyte of why this isn’t a cheat. A student familiar with conditional proof in a Fitch-style setting (where there is no requirement that the formula at the head of a subproof is essentially used in the derivation of the end-formula of the subproof) should have a head start in understanding what is going on in the Gentzen setting and why it might be thought unproblematic. Why not make the connection?

Next, it is worth saying that, while this chapter is about natural deduction proofs, there isn’t a single actual example of a proof set out! For the tree arrays which populate the chapter aren’t object language proofs, with formulas as assumptions and a formula as conclusion — they are all entirely schematic, with every featured expression a metalinguistic schema. Ok, this is pretty common practice; and it wouldn’t be worth remarking on if it was very clearly explained that this is what is happening. But it isn’t (I suppose a mis-stated single sentence back on p. 20 in the previous chapter is somehow supposed to do the job). And worse, our authors sometimes seem to themselves forget that everything is schematic. For example, at the foot of p. 79 an attempted proof schema is laid out, ending with the schema 𝐴(𝑐) ⊃ ∀𝑥𝐴(𝑥). This is followed by the comment “The end-formula of this ‘deduction’ is not valid, so it should not have a proof”. Now, it is indeed formulas, not schemas, that have natural deduction proofs according to the definition of a proof on p. 69. OK, so what is “the end-formula” here? There is  no unique such formula. Are we supposed to be generalising then about all formula-instances of the proof schema? But the end-formula of an instance of this attempted proof schema could perfectly well be valid. Ok, yes of course, it is easy to tidy this up so it says what is meant, along with a number of related mishaps: but the student reader shouldn’t be left having to do the work.

A third point. Oddly to my mind, the authors have decided to say nothing here about the supposed harmony between the core introduction and elimination rules shared by classical and intuitionist logic (there is just the briefest of mentions in the Preface of this as a topic that the reader might want to follow up). Well, I can certainly understand not wanting to get embroiled in the ramifying debates about the philosophical significance of harmony. But the relevant formal feature of the rules (that demarcates “or” from “tonk”) is so very neat that it is surely worth saying something about it, even when formal issues are at the forefront of attention. More generally — though I do realize this now is a rather unfocused grumble — I’d say that the expository §§3.1–3.4 don’t really bring out the elegance of Gentzen-style natural deduction.

Moving on to the rest of the chapter, §3.5 notes a couple of measures of the complexity of a deduction tree, and then the remaining two sections of the chapter look at a handful of results about deductions proved by induction on complexity. In particular, §3.7 shows that a formula is deducible in the axiomatic system for classical logic given in the previous chapter if and only if it is deducible in the classical natural deduction system described in this chapter. This bit of proof-theory is nicely done.

I’ve more quibbles that I’ll skip over. Overall, though, I would say that this chapter does fall somewhat short of my ideal of an introduction to Gentzen-style natural deduction. Still, students coming to it already knowing about Fitch-style proofs will surely be able to manage the transition and should get the hang of things pretty well. But I suspect that those who have never encountered a natural deduction system before might find it all significantly harder going.

To be continued

IPT is particularly aimed at those “who have only a minimal background in mathematics and logic”. Well, philosophy students who haven’t done much logic may well not have encountered an old-school axiomatic presentation of logic before. So — perhaps reasonably enough — Chapter 2 is on Axiomatic Calculi.  The chapter divides into two uneven parts, which I’ll take in turn.

In the early sections, we meet axiomatic versions of minimal, intuitionist and classical logic for propositional logic (presented using axiom schemas in the usual way). Next, after a pause to explain the idea of proofs by induction, there’s a proof of the deduction theorem, and an explanation of how to prove independence of axioms (more particularly, the independence of ex falso from minimal logic, and the independence of the double negation rule from intuitionist logic) using deviant “truth”-tables. Then we add axioms for predicate logic, and prove the deduction theorem again. So this part of the chapter is routine stuff. And really the only question is: how well does the exposition unfold?

By my lights, not very well. OK, perhaps the general state of the world is rather getting to me, and my mood is less than sunny. But I did find this disappointing stuff.

For a start, the treatment of schemas is a mess. It really won’t do to wobble between saying (p. 19) that axioms are formulas which are instances of schemas, and saying that such a formula is an instance of an axiom (p. 21). Or how about this: “an instance of an instance of an axiom is an axiom” (p. 21). This uses ‘axiom’ in two different senses (i.e. first meaning axiom schema) and then meaning axiom), and it uses ‘instance’ in two different senses (first meaning instance (of schema) and then meaning variant schema got by systematically replacing individual schematic letters by schemas for perhaps non-atomic wffs).

Or how about this? — We are told that a formula is a theorem just if it is the end-formula of a derivation (from no assumptions). We are immediately told, though, that “in general we will prove schematic theorems that go proxy for an infinite number of proofs of their instances.” (p. 20) You can guess what this is supposed to mean: but it isn’t what the sentence actually says. There’s more of the same sort of clumsiness.

When it comes to laying out proofs, things again get messy. The following, for example, is described as a derivation (p. 32):

This is followed by the comment “Note that lines 1 and 2 do not have a ⊢ in front of them. They are assumptions, not theorems. We indicate on the left of the turnstile which assumptions a line makes use of. For instance, line 4 is proved from lines 1 and 3, but line 3 is a theorem — it does not use any assumptions.” But first, with this sort of Lemmon-esque layout, shouldn’t the initial lines have turnstiles after all? Shouldn’t the first line commence, after the line number, with “(1) ⊢” — since the assumption that the line makes use of is itself? And more seriously, in so far we can talk of line (9) as being derived from what’s gone before, it is the whole line read in effect as a sequent which is derived from line (8) read as a sequent — it’s not an individual formula derived from earlier ones by a rule of inference. So in fact this just isn’t a derivation any more in the original sense given in IPT in characterizing axiomatic derivations.

I could continue carping like this but it would get rather boring. However, a careful reader will find more to quibble about in these sections of the chapter, and — more seriously — a student coming to them fresh could far too easily be misled/confused.

The final long §2.15, I’m happy to say, is a rather different kettle of fish, standing somewhat apart from the rest of the chapter in both topic and level/quality of presentation. This section can be treated pretty much as a stand-alone introduction to a key fact about classical and intuitionist first-order Peano Arithmetic (with an axiomatic logic), namely that we can interpret the first in the second, thereby establishing that classical PA is consistent if the intuitionist version is. This is, I think, neatly done enough (though I suspect the discussion might need a slightly more sophisticated reader than what’s gone before).

Just one very minor comment. A student might wonder why what is here called the Gödel-Gentzen translation (atoms are left untouched) is different from what many other references call the Gödel-Gentzen translation (where atoms are double negated). A footnote of explanation might have been useful. But as I say, this twelve page section seems much better.

To be continued