Sequents and Trees: An Introduction to the Theory and Applications of Propositional Sequent Calculi

Preface
Acknowledgments
Contents
1 Analytic Sequent Calculus for CPL
	1.1 The Classical Propositional Calculus
		1.1.1 Language
		1.1.2 Semantics
		1.1.3 Axiomatization
	1.2 Sequent Calculus
		1.2.1 Sequents and their Interpretation
		1.2.2 System K
	1.3 Proofs and Derivations
		1.3.1 Constructing Proofs
		1.3.2 Disproofs
		1.3.3 Analyticity
	1.4 Additional Rules
		1.4.1 Rules for Other Connectives
		1.4.2 Derivability and Admissibility
		1.4.3 Invertibility of Rules
	1.5 The Adequacy of K
	1.6 Decidability
		1.6.1 Proof Trees
		1.6.2 Confluency
		1.6.3 Decidability
	1.7 An Analytic Proof of Completeness
		1.7.1 Hintikka's Tuples
		1.7.2 Completeness
	1.8 The Cut Rule
		1.8.1 Admissibility versus Eliminability
		1.8.2 Admissibility of Cut
	1.9 Applications of Cut
		1.9.1 Equivalence with Axiomatic Formulation of CPL
		1.9.2 Equivalence of Tarskian Consequence Relations
	1.10 Completeness Again
		1.10.1 Consistency
		1.10.2 Maximality
		1.10.3 Completeness
		1.10.4 Some Variant Proofs
	1.11 Restricted Cut
		1.11.1 Completeness with Analytic Cut
		1.11.2 Constructive Proof of Analytic Cut Admissibility
		1.11.3 Proof Search
		1.11.4 Strong Completeness
		1.11.5 Interpolation Theorem
2 Gentzen's Sequent Calculus LK
	2.1 The System LK
		2.1.1 Rules
		2.1.2 Proofs
	2.2 Applications of Cut
		2.2.1 Equivalent Sequents
		2.2.2 Equivalent Rules
	2.3 Syntactical Invertibility
	2.4 Local Proofs of Cut Elimination
		2.4.1 Gentzen's Proof
		2.4.2 Cross-Cuts Technique
		2.4.3 Reductive Proof
		2.4.4 Contraction-Sensitive Proof
	2.5 Global Proofs of Cut Elimination
		2.5.1 Curry's Substitutive Proof
		2.5.2 Buss' Invertive Proof
	2.6 Decidability
	2.7 Permutability of Rules
3 Purely Logical Sequent Calculus
	3.1 The System G3
	3.2 Preliminary Results
		3.2.1 Invertibility Again
		3.2.2 Admissibility of Contraction
	3.3 Admissibility of Cut
		3.3.1 Dragalin's Proof
		3.3.2 Smullyan's Proof
		3.3.3 Schütte's Proof
		3.3.4 Schütte-style Proof for Admissibility of A-cut
	3.4 Interpretations of Sequents
		3.4.1 Post Theorem
		3.4.2 SC and Other Kinds of Systems
	3.5 Variants of SC
		3.5.1 Types of Sequents
		3.5.2 Generalised SC
		3.5.3 Ordinary SC
		3.5.4 Gentzen's Type of Ordinary SC
		3.5.5 Standard SC
	3.6 Constructive Proofs of Interpolation Theorem
		3.6.1 Maehara's Proof
		3.6.2 Smullyan's Proof
		3.6.3 Interpolation by Splitting a Proof
	3.7 Some Related Results
		3.7.1 Tautology Elimination Rule
		3.7.2 Strong Completeness in Normal Form
4 Sequent Calculi for Modal Logics
	4.1 Basic Modal Logics
		4.1.1 Hilbert Systems
		4.1.2 Relational Semantics
	4.2 SC for Modal Logics
		4.2.1 Modal Extensions of LK
		4.2.2 Modal Extensions of G3
		4.2.3 Rules for Diamonds
	4.3 Cut Elimination
		4.3.1 Mix Elimination for LKT, LKS4
		4.3.2 Admissibility of Cut in G3T and G3S4
	4.4 Decidability
		4.4.1 Proof Search in G3T
		4.4.2 Completeness of G3T
		4.4.3 Proof Search in G3S4
		4.4.4 Modal Logic with Simplified Proof Search Tree
	4.5 The Case of S5
		4.5.1 Cut-free and Cut-restricted Solutions
		4.5.2 Indirect Solutions
	4.6 Generalised SC
		4.6.1 Labelled Sequent Calculi
		4.6.2 Simple Labelled System
	4.7 Hypersequent Calculus
		4.7.1 The Basic HC
		4.7.2 Systems for S5
		4.7.3 Admissibility of Cut
	4.8 Pairs of Sequents are Sufficient
		4.8.1 Sato's Structured System
		4.8.2 Double Sequent Calculus
		4.8.3 Bisequent Calculi
5 Alternatives to CPL
	5.1 Intuitionistic Logic
		5.1.1 Relational Semantics
		5.1.2 Gentzen's Characterisation of INT
		5.1.3 Other Variants of SC
	5.2 Substructural Logics
		5.2.1 The Significance of Structural Rules
		5.2.2 Linear Logic
	5.3 Relevant Logics
		5.3.1 SC for Relevant Logics
		5.3.2 Generalised Sequent Calculi for Relevant Logics
		5.3.3 First-Degree Entailment
	5.4 Many-Valued Logics
		5.4.1 The Basic Logics
		5.4.2 Proof Theory
		5.4.3 Standard SC for Many-Valued Logics
	5.5 Generalised Sequent Calculi
		5.5.1 N-sided Systems as Structured Sequents
		5.5.2 A More Uniform Approach to Structured Sequents
		5.5.3 Cut Admissibility
Appendix