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.
No comments:
Post a Comment