product iamge

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

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

Author(s): Alex K. Simpson
Publisher: University of Edinburgh
Year: 1994

Language: English
Pages: 219

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