Synopses & Reviews
'This excellent introduction to the basic ideas of structural proof theory--the theory of formal proofs as combinatorial structures--uses cut elimination and normalization as central tools. The authors thoroughly discuss and compare various types of formalization of first-order logic, in particular Hilbert systems, Gentzen systems, and Natural Deduction. They give examples of several application areas namely, the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic; and second-order logic. In each case Troelstra and Schwichtenberg illustrate the methods in relatively simple situations and then apply them elsewhere in more complex settings. The chapters feature numerous exercises for student practice. With the only prerequisite a standard course in first-order logic, the book is ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science, and artificial intelligence.'
Review
'This is a fine book. Any computer scientist with some logical background will benefit from studying it. It is written by two of the experts in the field and comes up to their usual standards of precision and care.' Ray Turner, Computer Journal
Synopsis
Introduction to proof theory and its applications in mathematical logic, theoretical computer science and artificial intelligence.
Synopsis
This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of first-order logic formalization. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic, logic programming theory, category theory, modal logic, linear logic, first-order arithmetic and second-order logic. In each case the authors illustrate the methods in relatively simple situations and then apply them elsewhere in much more complex settings. For the new edition, they have rewritten many sections to improve clarity, added new sections on cut elimination, and included solutions to selected exercises. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence.
Synopsis
This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included.
Synopsis
This is an introduction to the basic ideas of structural proof theory. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included.
Description
Includes bibliographical references (p. 379-403) and index.
Table of Contents
1. Introduction; 2. N-systems and H-systems; 3. Gentzen systems; 4. Cut elimination with applications; 5. Bounds and permutations; 6. Normalization for natural deduction; 7. Resolution; 8. Categorical logic; 9. Modal and linear logic; 10. Proof theory of arithmetic; 11. Second-order logic; Solutions to selected exercises. Bibliography; Symbols and notation; Index.