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