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

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