A Introduction to Proof Theory, Ch. 5.
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 sets or 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 nice 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 a regimented theory of deducibility!
Now, 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 nice 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 in the nice opening chapter ‘From Natural Deduction to Sequent Calculus’ of Jan von Plato and Sara Negri’s Structural Proof Theory (CUP, 2001). At the least, it would be good to ease the student in by starting with some natural deduction proofs and their sequent calculus analogues, to give a sense of how things work. But as it is, after setting up the calculus, IPT dives straight in to consider 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! However, the discussion does give some plausibility to the claim that provable sequents should be provable without cut.
Cut elimination is 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.
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, then, 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
The post A Introduction to Proof Theory, Ch. 5. appeared first on Logic Matters.
