Question

I'm looking for a good introductory resource on sequent calculus suitable for someone who has studied natural deduction before. Books and online resources are both OK, as long as each rule of inference and any notational convention is explained. Thanks.

Answer 1

Girard's Proofs and Types contains a good intro to this stuff. A translation to English by Paul Taylor and Yves Lafont is available free online. I also like Negri and van Plato's Structural Proof Theory and have heard good things about Troelstra and Schwichtenberg's Basic Proof Theory.

Answer 2

You can read the chapter on Sequent Calculus from Frank Pfenning's manuscript on Automated Theorem Proving. This chapter builds towards an explanation of sequent calculus by way of its relationship to natural deduction.

Answer 3

Gentzen, 1934, 'Investigations into Logical Deduction' — This is very readable, and introduces so many ideas that later synthetic works invariably miss some. If you're serious, this, and some other papers of Gentzen's, are indispensable.

Stan Wainer has written some excellent introductory texts. I don't think any are freely available for download, although PDFs are washing about here and there. Wainer, 1997, 'Basic Proof Theory with Applications to Computation', in Schwichtenberg, Logic of Computation, Springer Verlag, I strongly recommend.

But the best starting point is probably Proofs and Types, as recommended by Neel, reading at least up to the proof of cut elimination. A warning: Girard's style is a little slippery, and it is common for students to say they have read it, who turn out to have absorbed the opinions but little of the results.

Postscript — If you care about the fine technicalities of matching up normal proofs in natural deductions with cut-free proofs in sequent calculus, Ungar, 1992 Normalization, cut-elimination, and the theory of proofs is a good text, generously made freely available as part of the Stanford Medieval and Modern Thought Digitization Project. This literature is a bit tricky, because the two proof calculi are formulated, and their metatheory have come about in a somewhat different manner. The literature doesn't date back to Gentzen, except to the trivial extent that the two calculi are shown to have equivalent expressive strength, because the theory of normalisation for natural deduction was not fixed untilo Prawitz, 1965, Natural Deduction.

Answer 4

I would recommend reading Sara Negri's "Five lectures on Proof Analysis" that you can find here http://www.helsinki.fi/~negri/prana.pdf. In the first lecture she tries to obtain sequent calculus from natural deduction very naturally (of course, by making hypotheses explicit).

Answer 5

If you are looking for a source on basic sequent calculus, both propositional and first-order logic---by which I mean the basic definitions, explanations, and basic theorems (like cut-elimination), and all this developed from scratch and in a very readable way, with all notations explained---I would recommend the book of Cook and Nguyen, Logical Foundations of Proof Complexity (2010, Cambridge University Press, ASL Perspectives in Logic).

An online draft (which is almost identical to the book) is here.

What you'll need to read is only Chapter 2:

The Predicate Calculus and the System LK: Propositional calculus, Gentzen’s propositional proof system PK, Soundness and completeness of PK, PK proofs from assumptions, Propositional compactness, Predicate calculus, Syntax of the predicate calculus, Semantics of predicate calculus, The first-order proof system LK, Free variable normal form, Completeness of LK without equality, Equality axioms, Equality axioms for LK, Revised soundness and completeness of LK, Major corollaries of completeness, The Herbrand Theorem.

Answer 6

I second here the recommendations of Troelstra and Schwichtenberg's Basic Proof Theory for learning sequent calculus because of its exercises; focus on chapter 3 and do the exercises to get a good grip on standard sequent calculi for classical and intuitionistic logic, as well as get some exposure to a few variations (e.g., single-sided calculi). von Plato and Negri's Structural Proof Theory is also very good, but it is more of a monograph than a textbook (there are no exercises). In von Plato and Negri you will find detailed and systematic discussion of the relationship between natural deduction and sequent calculi throughout the book, a discussion that is is largely missing from Troelstra and Schwichtenberg (though it must be said that T and S do prove that various sequent calculi are equivalent with natural deduction and with certain Hilbert/Frege-style proof systems).