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