The Proof Theory and Semantics of Intuitionistic Modal Logic [PhD Thesis]

✍ Scribed by Alex K. Simpson

• Publisher: University of Edinburgh
• Year: 1994
• Tongue: English
• Leaves: 219
• Category: Library

✦ Table of Contents

1. Introduction 1
   1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
   1.2 Synopsis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2. Intuitionistic logic 9
   2.1 Natural deduction for intuitionistic logic . . . . . . . . . . . . . . . 9
   2.1.1 The natural deduction system . . . . . . . . . . . . . . . . . 9
   2.1.2 Normalization . . . . . . . . . . . . . . . . . . . . . . . . . . 13
   2.2 The semantics of intuitionistic logic . . . . . . . . . . . . . . . . . . 20
   2.3 Geometric theories in intuitionistic logic . . . . . . . . . . . . . . . 24
3. Intuitionistic modal logic 32
   3.1 Modal logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
   3.2 What is intuitionistic modal logic? . . . . . . . . . . . . . . . . . . 38
   3.3 Previous approaches to intuitionistic modal logic . . . . . . . . . . . 41
   3.4 Our approach to intuitionistic modal logic . . . . . . . . . . . . . . 58
4. Natural deduction for intuitionistic modal logics 65
   4.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
   4.2 The basic modal natural deduction system . . . . . . . . . . . . . . 70
   4.3 Conditions on the visibility relation . . . . . . . . . . . . . . . . . . 72
   4.4 The consequence relation . . . . . . . . . . . . . . . . . . . . . . . . 76
   4.5 Soundness relative to modal models . . . . . . . . . . . . . . . . . . 78
   4.6 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
5. Meta-logical completeness 85
   5.1 Meta-logical soundness . . . . . . . . . . . . . . . . . . . . . . . . . 86
   5.2 A semantics for intuitionistic modal logics . . . . . . . . . . . . . . 88
   5.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
   5.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
6. Axiomatizations 98
   6.1 Correspondence with IK . . . . . . . . . . . . . . . . . . . . . . . . 98
   6.2 Axiomatizations of other modal logics . . . . . . . . . . . . . . . . . 105
   6.3 Problems with a more general scheme . . . . . . . . . . . . . . . . . 111
   6.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
7. Normalization and its consequences 118
   7.1 Strong normalization for N(T ) . . . . . . . . . . . . . . . . . . . 118
   7.2 A cut-free sequent calculus . . . . . . . . . . . . . . . . . . . . . . . 125
   7.3 Decidability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
   7.3.1 The structure of sequents . . . . . . . . . . . . . . . . . . . 134
   7.3.2 A preorder on sequents . . . . . . . . . . . . . . . . . . . . . 138
   7.3.3 Irredundant derivations and decidability . . . . . . . . . . . 142
   7.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
8. Birelation models and the finite model property 148
   8.1 Interpreting N in birelation models . . . . . . . . . . . . . . . . . 148
   8.1.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . 150
   8.1.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
   8.1.3 Extension to N(T ) . . . . . . . . . . . . . . . . . . . . . . 155
   8.2 The finite model property . . . . . . . . . . . . . . . . . . . . . . . 157
   8.2.1 Constructing a bounded model . . . . . . . . . . . . . . . . 161
   8.2.2 Quotienting a birelation model . . . . . . . . . . . . . . . . 167
   8.2.3 Applying the quotienting technique . . . . . . . . . . . . . . 171
   8.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174
9. Conclusions and further work 176
   9.1 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
   9.2 Further work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
   A. Proofs of strong normalization and confluence for NIL(T ) 182
   A.1 Proof of strong normalization . . . . . . . . . . . . . . . . . . . . . 182
   A.2 Proof of confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . 190
   B. Sequence prefixes 194