Proof Theory: Sequent Calculi and Related Formalisms

Proofs and proof theory Proofs of all kinds Early history of proof theory in a nutshell Proofs as calculations Classical first-order logic The sequent calculus LK An axiom system for FOL Equivalence of LK and K Interpretations, soundness and completeness Variants of the first sequent calculi Intuitionistic logic and other modifications Sequent calculi with multisets and sets Sequent calculi with no structural rules One-sided sequent calculi Uniform sequent calculi Disjunction property Translations between classical and intuitionistic logics Sequent calculi for non-classical logics Associative Lambek calculus Extensions of the associative Lambek calculus Relevant implication and pure entailment Non-distributive logic of relevant implication Linear logic Positive logic of relevant implication Sequent calculi for modal logics Merge calculi Consecution calculi for non-classical logics Non-associative Lambek calculus Structurally free logics More implicational relevance logics Positive entailment logics Calculi with multiple right-hand side Display calculi and hypersequents Display logics with star Display logic for linear logic Display logic for symmetric gaggles Hypersequent calculi Cut rules and cut theorems Uniform cut theorem Mix, multiple and single cuts Constants and the cut Display cut Cut theorem via normal proofs Cut theorem via interpretations Analytic cut Consequences of the cut theorem and uses of the cut rules Some other proof systems Natural deduction systems Tableau systems Resolution systems Applications and applied calculi Decidability Sequent calculi for mathematical theories Typed and labeled calculi Appendix: Some supplementary concepts Bibliography Index