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.
$\begingroup$
$\endgroup$
1
asked Feb 9, 2010 at 13:39
-
$\begingroup$ A really interactive, accessible, but short introduction is available: logitext.mit.edu/logitext.fcgi/tutorial $\endgroup$– Janus TroelsenFeb 10, 2014 at 1:41
Add a comment
|
6 Answers
$\begingroup$
$\endgroup$
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.
answered Feb 9, 2010 at 13:47
-
1$\begingroup$ I'll second Proofs and Types. I'm not a big fan of Negri&von Plato; Troelstra & Schwichtenberg cover a lot of ground, have good history sections, and introduce a useful (but far from complete) categorisation of kinds of sequent calculi. $\endgroup$ Feb 10, 2010 at 6:55
$\begingroup$
$\endgroup$
2
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 until Prawitz, 1965, Natural Deduction.
-
$\begingroup$ I don't think Gentzen makes clear this translation from Natural Deduction to Sequent Calculus although he discovered it. $\endgroup$ Jul 1, 2010 at 17:22
-
$\begingroup$ @Charles: By "translation" I meant the actual way Gentzen came up with sequent calculus. Of course, the main idea was to make hypotheses in ND proofs explicit, but in Gentzen(1934) he didn't explain in detail how he came up with the rules of sequent calculus he described (exept cut rule, they are all increasing w.r.t. subformula property, however, obvious way of making hypotheses explicit leads to some decreasing rules for every connective, which correspond to ND elimination rules) and with cut elimination. $\endgroup$ Jul 6, 2010 at 2:07
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
2
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).
answered Jul 1, 2010 at 17:42
-
$\begingroup$ For modern treatment of the main results, such as Cut Elimination and its consequences (Consistency, Herbrand's theorem, Craig Interpolation and Beth Definability) see Samuel Buss's elegant paper "An introduction to proof theory" (be careful, the paper contain some errors, for instance, the proof of Generalization of Herbrand's theorem is wrong). $\endgroup$ Jul 1, 2010 at 17:54
-
$\begingroup$ @Sergei: I'd recommend getting the book, Negri & von Plato, 2001, Structural proof Theory to someone who wants to study this approach, which emphasises the generalised elimination rules of Schröder-Heister, cf. e.g., www-ls.informatik.uni-tuebingen.de/psh/forschung/publikationen/… $\endgroup$ Jul 5, 2010 at 12:55
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
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).
