Gentzen Calculi for Modal Propositional Logic (eBook)

Preface 6
Contents 10
Part I An Overview of the Sequent Calculus 13
1 What Is a Good Sequent Calculus? 14
1.1 The Sequent Calculus Gcl 14
1.2 Formal Remarks 18
1.3 Philosophical Remarks 23
1.3.1 Analyticity 23
1.3.2 Logicality 25
1.3.3 From Logicality to Inferentialism 27
1.3.4 Harmony 29
1.3.5 Inferentialism 31
1.3.6 Concluding Remarks 32
1.4 Subformula Property 33
1.5 Admissibility of the Structural Rules 35
1.5.1 Operational vs Global Meaning 37
1.6 Admissibility of the Logical Rules 39
1.7 Explicitness, Separation and Symmetry 39
1.8 Uniqueness 40
1.9 Syntactic Purity 40
1.10 Došen's Principle Redefined 42
1.10.1 Modularity 45
Notes 45
Part II Sequent Calculi for Modal Logic 47
2 Modal Logic and Ordinary Sequent Calculi 48
2.1 Normal Modal Logic 48
2.2 Ordinary Sequent Calculi for Modal Logic 54
2.3 The Idea of Generalising the Gentzen Calculus 60
Notes 62
3 Purely Syntactic Methods 63
3.1 Multiple Sequent Calculi 64
3.2 Higher-Arity Sequent Calculi 70
3.3 Display Sequent Calculi 74
Notes 62
4 Semantic Methods 83
4.1 Semantic Modal Sequent Calculi 84
4.2 Indexed Sequent Calculi 92
4.3 Internalised Forcing (Relation) Sequent Calculi 100
Notes 108
5 Comparing the Different Generalisations of the Sequent Calculus 109
5.1 From Multiple Sequent Calculi to Display Sequent Calculi 109
5.2 From Higher-Arity Sequent Calculi to Display Sequent Calculi 112
5.3 From Indexed Sequent Calculi to Internalised Forcing Sequent Calculi 115
5.4 From Indexed Sequent Calculi to Semantic Modal Sequent Calculi and Vice Versa 120
5.5 From Display Sequent Calculi to Internalised Forcing Sequent Calculi 121
Notes 124
Part III Tree-Hypersequent Calculi 125
6 On the Tree-Hypersequent Calculi 126
6.1 The Calculi Thsk* 129
6.2 Logical Variant of the Tree-Hypersequent Calculi 133
6.3 Adequacy of the Tree-Hypersequent Calculi 145
Notes 148
7 Syntactic Cut-Admissibility and Decidability 149
7.1 Cut-Admissibility in the Tree-Hypersequent Calculi 149
7.2 Decidability of the Tree-Hypersequent Calculi 162
Notes 169
8 Semantic Adequacy 170
8.1 Semantic Validity of the Tree-Hypersequent Calculi 170
8.2 Semantic Completeness of the Tree-Hypersequent Calculi 175
9 A Hypersequent Calculus for the System S5 180
9.1 The Calculus ThS5L 181
9.2 Admissibility of the Structural Rules in ThS5L 182
9.3 Adequacy of ThS5L 185
9.4 Cut-Admissibility in ThS5L 186
9.5 Decidability of ThS5L 188
Notes 191
10 A Tree-Hypersequent Calculus for the Modal Logic of Provability 192
10.1 The Calculus ThsglL 192
10.2 Admissibility of the Structural Rules in ThsglL 193
10.3 Adequacy of ThsglL 198
10.4 Cut-Admissibility in ThsglL 201
11 Further Results on Tree-Hypersequent Calculi 207
11.1 Tree-Hypersequent Calculi and Other Calculi 207
11.2 Tree-Hypersequent Calculi and Other Logics 210
11.3 Tree-Hypersequent Calculi and Further Developments 211
Note 211
References 212
Symbols and Notations 218
Index 221