scientific article; zbMATH DE number 1497485
apartnesscategorical logicclassical logiccoherence theoremcombinatory logicconnections with computer sciencecut eliminationE-logicfirst-order arithmeticformulas-as-types relationGentzen type systemHilbert-style systeminterpolationintuitionistic logicKleene-style sequent calculuslinear logiclogic programmingminimal logicmodal logicmulti-succedent intuitionistic sequent calculusnatural deduction systemproof theoryresolutionsecond-order Heyting arithmeticsequent calculusstrong normalizationtype theory
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30) Logic programming (68N17)
The book under review is the second edition of this almost encyclopaedic monograph on proof theory [for a review of the first edition (ibid. 1996) see Zbl 0868.03024], which was thoroughly revised and slightly extended. It treats structural proof theory in depth, and everybody interested in this subject should study it. However one should be aware that the authors chose deliberately to take only a first glimpse at mathematical proof theory (proof theory of axiom systems for formalizing fragments of mathematics), and that the reader interested in this topic should refer to standard text books on proof theory [\textit{K. Schütte}, Beweistheorie, Die Grundlehren der mathematischen Wissenschaften. 103. Berlin-Göttingen-Heidelberg: Springer-Verlag (1960; Zbl 0102.24704); \textit{K. Schütte}, Proof theory. Translation from the German by J. N. Crossley, Grundlehren der mathematischen Wissenschaften. 225. Berlin-Heidelberg-New York: Springer-Verlag (1977; Zbl 0367.02012); \textit{G. Takeuti}, Proof theory, Studies in Logic and the Foundations of Mathematics. 81. Amsterdam-Oxford: North-Holland Publishing Company; New York: American Elsevier Publishing Company, Inc. (1975; Zbl 0354.02027 and Zbl 0355.02023); Second edition: ibid., Amsterdam etc.: North-Holland Publishing Co. (1987; Zbl 0609.03019); \textit{J.-Y. Girard}, Proof theory and logical complexity. Volume I. Studies in Proof Theory. Monographs 1. Napoli: Bibliopolis. Edizioni di Filosofia e Scienze (1987; Zbl 0635.03052); \textit{W. Pohlers}, Proof theory. An introduction. Lecture Notes in Mathematics 1407. Berlin etc.: Springer-Verlag (1989; Zbl 0695.03024); \textit{G. Jaeger}, Theories for admissible sets. A unifying approach to proof theory. Studies in Proof Theory. Lecture Notes, 2. Napoli: Bibliopolis (1986; Zbl 0638.03052); \textit{W. Buchholz} and \textit{K. Schütte}, Proof theory of impredicative subsystems of analysis. Studies in Proof Theory, Monographs, 2. Napoli: Bibliopolis (1988; Zbl 0653.03039); \textit{S. R. Buss} (ed.), Handbook of proof theory. Studies in Logic and the Foundations of Mathematics. 137. Amsterdam: Elsevier (1998; Zbl 0898.03001)]. Apart from corrections of some unfortunate typos in the first edition -- it is recommended to use the second edition instead of the first one -- the following modifications have been carried out: in the overview 1.3 of the three types of formalisms (natural deduction, sequent calculus and Hilbert systems), natural deduction is now motivated via the BHK-interpretation and the sequent calculus is introduced as a way of constructing natural deduction derivations. This is helpful for the reader new to the subject. A chapter (2.1.10) on the representation of the complete discharge convention (CDC) in natural deduction with sequents has been added. The section on Kleene-style sequent calculus (3.5.11) has been extended and multi-succedent versions of the intuitionistic sequent calculus (3.5.10) together with a sketch of cut-elimination (4.1.10) have been added. A new section (3.4) with a general treatment of deduction systems with local rules has been introduced. The proof of the cut elimination theorem (4.1.5) has been revised (there are some tiny but misleading typos in this section, see the list of corrections mentioned below). Cut elimination results for extensions of the sequent calculus by rules (4.6), equality (4.7) and apartness (4.8) have been added. A result on the growth of size of proofs in propositional logic under cut elimination (5.2) has been included. Extensions of natural deduction systems with extra rules (6.4) are now treated and the section on E-logic (6.5) has been revised. The proof of strong normalization of system F (\(\lambda 2\)) makes now use of simplified techniques taken from [\textit{R. Matthes}, Extensions of system F by iteration and primitive recursion on monotone inductive types. München: Utz Verlag. München: LMU, Univ. München, Fakultät Mathematik/Informatik (1998; Zbl 0943.68086)]. Solutions to selected exercises have been added. A small criticism of the book might be that by treating sequents as multisets of formulas instead of sets, proofs become more involved, and therefore the reader might get the impression that cut elimination for the predicate calculus is more difficult than it really is. Further, the variety of systems (esp. G1--G3 and GK) might be more irritating rather than helpful. In order to see the simplicity of concepts, it would as well have been nice to mention the almost trivial proof of cut elimination for the (classical) Tait calculus, which is unfortunately called Gentzen-Schütte system in this book. In a book of such length almost inevitably some typos occur. A list of corrections is available from \url{http://www.mathematik.uni-muenchen.de/~schwicht/}.
- Proof theory for admissible rules
- Glivenko theorems revisited
- Let Us investigate! Dynamic conjecture-making as the formal logic of abduction
- Contraction, infinitary quantifiers, and omega paradoxes
- Prehistoric graph in modal derivations and self-referentiality
- A simple sequent calculus for Angell's logic of analytic containment
- Four-valued paradefinite logics
- Cut elimination, identity elimination, and interpolation in super-Belnap logics
- Eliminating disjunctions by disjunction elimination
- A semantic framework for proof evidence
- Proof theory for functional modal logic
- Anything goes
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- Elementary arithmetic
- Multicomponent proof-theoretic method for proving interpolation properties
- Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
- A spatial logic for concurrency. II
- Glivenko theorems and negative translations in substructural predicate logics
- The power of Belnap: sequent systems for \(SIXTEEN_{3 }\)
- Sequent calculi for intuitionistic Gödel-Löb logic
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- Cut-elimination for weak Grzegorczyk logic Go
- Recapturing dynamic logic of relation changers via bounded morphisms
- Subatomic negation
- What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
- On nonmonotonic consequence relations
- The implicit commitment of arithmetical theories and its semantic core
- The middle ground-ancestral logic
- Efficient SAT-based proof search in intuitionistic propositional logic
- A note on the unprovability of consistency in formal theories of truth
- The calculus of natural calculation
- Human-centered automated proof search
- Induction and Skolemization in saturation theorem proving
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
- SAT-based proof search in intermediate propositional logics
- Natural deduction systems for intuitionistic logic with identity
- A binary quantifier for definite descriptions for cut free free logics
- Normalisation and subformula property for a system of classical logic with Tarski's rule
- The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
- Logic and majority voting
- Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
- From input/output logics to conditional logics via sequents -- with provers
- Game semantics for constructive modal logic
- Sequent calculi for the propositional logic of HYPE
- Combinatory logic with polymorphic types
- Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
- A note on cut-elimination for classical propositional logic
- Uniform Lyndon interpolation for basic non-normal modal logics
- Constructive and mechanised meta-theory of intuitionistic epistemic logic
- Coherence in inquisitive first-order logic
- From truth degree comparison games to sequents-of-relations calculi for Gödel logic
- Essential structure of proofs as a measure of complexity
- Interpolation in extensions of first-order logic
- A type-assignment of linear erasure and duplication
- Herzberger's limit rule with labelled sequent calculus
- Relative full completeness for bicategorical Cartesian closed structure
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
- Modal and intuitionistic variants of extended Belnap-Dunn logic with classical negation
- Natural deduction bottom up
- Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization
- A simple logic of functional dependence
- Proof-theoretic semantics and inquisitive logic
- Labelled sequent calculi for Lewis' non-normal propositional modal logics
- Extended fuzzy constructive logic
- Proofs and countermodels in non-classical logics
- Speech acts, categoricity, and the meanings of logical connectives
- Hypersequent and display calculi -- a unified perspective
- Noncontractive classical logic
- Absorbing the structural rules in the sequent calculus with additional atomic rules
- Mechanizing focused linear logic in Coq
- Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
- Constructibility of the universal wave function
- Soundness and completeness proofs by coinductive methods
- The Church-Fitch knowability paradox in the light of structural proof theory
- Montague's paradox, informal provability, and explicit modal logic
- \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs
- Sufficient conditions for cut elimination with complexity analysis
- Making knowledge explicit: how hard it is
- Logic of subtyping
- Computing interpolants in implicational logics
- Incomplete symbols -- definite descriptions revisited
- A simple proof of second-order strong normalization with permutative conversions
- The naturality of natural deduction
- Asymptotic distribution of integers with certain prime factorizations
- On rules
- On structural contraction and why it fails
- The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract)
- Intuitionistic propositional logic with Galois negations
- Notes on models of (partial) Kripke-Feferman truth
- Positive logic with adjoint modalities: proof theory, semantics and reasoning about information
- Glivenko sequent classes in the light of structural proof theory
- Imperative LF meta-programming
- Cut elimination for GLS using the terminability of its regress process
- Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective)
- Sharpened lower bounds for cut elimination
- On the complexity of proof deskolemization
- Tools for the investigation of substructural and paraconsistent logics
- An evaluation-driven decision procedure for G3i
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4499084)
