The Proof Theory and Semantics of Intuitionistic Modal Logic Alex K. Simpson Doctor of Philosophy University of Edinburgh 1994 (Graduation date November 1994) Abstract Possible world semantics underlies many of the applications of modal logic in computerscienceandphilosophy. Thestandard theoryarisesfrominterpretingthe semanticde(cid:12)nitionsintheordinarymeta-theoryofinformalclassicalmathematics. If,however,thesame semanticde(cid:12)nitionsare interpretedinan intuitionisticmeta- theory then the induced modal logics no longer satisfy certain intuitionistically invalid principles. This thesis investigates the intuitionistic modal logics that arise in this way. Natural deductionsystems for various intuitionisticmodal logicsare presented. From one point of view, these systems are self-justifying in that a possible world interpretationof themodalities can be read o(cid:11) directlyfrom the inferencerules. A technical justi(cid:12)cation is given by the faithfulness of translations into intuitionistic (cid:12)rst-order logic. It is also established that, in many cases, the natural deduction systemsinducewell-knownintuitionisticmodal logics, previouslygivenbyHilbert- style axiomatizations. Themainbene(cid:12)tof thenaturaldeductionsystemsoveraxiomatizationsistheir susceptibilitytoproof-theoretictechniques. Strongnormalization(andconfluence) results are proved for all of the systems. Normalization is then used to establish the completeness of cut-free sequent calculifor all of the systems, and decidability for some of the systems. Lastly, techniques developed throughout the thesis are used to establish that those intuitionistic modal logics proved decidable also satisfy the (cid:12)nite model property. For the logics considered, decidability and the (cid:12)nite model property presented open problems. i Acknowledgements I owe much to my supervisor, Gordon Plotkin. Not only has he taught me a great deal, but he has been enormously supportive throughout my ‘random walk’ towards a thesis. I am indebted to my former colleagues, Fausto Giunchiglia and Luciano Ser- a(cid:12)ni, for provoking my initial interest in modal logic. They have remained rich sources of ideas and intellectual stimulation. The work in this thesis has bene(cid:12)ted greatly from discussions with Valeria de Paiva, David Pym and Colin Stirling. The presentation of the thesis has bene(cid:12)ted from the use of Paul Taylor’s Latex diagram package. The Laboratory for the Foundations of Computer Science has provided a very stimulating (and distracting) environment for research. It has been my pleasure to discuss many subjects with many people. I mentionin particular the Ben Alder team: John Longley, Savi Maharaj and Pete Sewell. I also thank my o(cid:14)ce mates, PietroCenciarelli,ChristopheRa(cid:11)alliandAndrewWilson,for toleratingthemany moods of writing up. Above all, I thank my family and friends for their love and support over the last three years. This thesis is dedicated to the memory of my grandfather, Tom Edward Lewis. ii Declaration This thesis was composed by myself, and the work reported herein is my own. iii 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 iv Table of Contents v 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 (cid:3)(cid:6) 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 Table of Contents vi 8. Birelation models and the (cid:12)nite model property 148 8.1 Interpreting N in birelation models : : : : : : : : : : : : : : : : : 148 (cid:3)(cid:6) 8.1.1 Completeness : : : : : : : : : : : : : : : : : : : : : : : : : : 150 8.1.2 Soundness : : : : : : : : : : : : : : : : : : : : : : : : : : : : 153 8.1.3 Extension to N (T ) : : : : : : : : : : : : : : : : : : : : : : 155 (cid:3)(cid:6) 8.2 The (cid:12)nite 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 N (T ) 182 IL A.1 Proof of strong normalization : : : : : : : : : : : : : : : : : : : : : 182 A.2 Proof of confluence : : : : : : : : : : : : : : : : : : : : : : : : : : : 190 B. Sequence pre(cid:12)xes 194 List of Figures 2{1 Natural deduction for intuitionistic predicate logic. : : : : : : : : : 11 2{2 Proper reductions. : : : : : : : : : : : : : : : : : : : : : : : : : : : 14 2{3 Permutative reductions. : : : : : : : : : : : : : : : : : : : : : : : : 14 2{4 Derivation of (cid:31) from (R ). : : : : : : : : : : : : : : : : : : : : : : : 26 (cid:31) 2{5 Derivation of (R ) from (cid:31). : : : : : : : : : : : : : : : : : : : : : : : 26 (cid:31) 2{6 Permutative reduction for (R ). : : : : : : : : : : : : : : : : : : : : 26 (cid:31) 3{1 The modal logic K. : : : : : : : : : : : : : : : : : : : : : : : : : : : 35 3{2 Modal axioms and corresponding frame properties. : : : : : : : : : 35 3{3 Intuitionistic K without (cid:6). : : : : : : : : : : : : : : : : : : : : : : : 46 3{4 Wijesekera’s system. : : : : : : : : : : : : : : : : : : : : : : : : : : 47 3{5 Countermodel to Requirement 3. : : : : : : : : : : : : : : : : : : : 48 3{6 Axiomatization of IK. : : : : : : : : : : : : : : : : : : : : : : : : : 52 3{7 Intuitionistic modal axioms. : : : : : : : : : : : : : : : : : : : : : : 56 4{1 The basic modal natural deduction system, N . : : : : : : : : : : 69 (cid:3)(cid:6) 4{2 Derivations of the IK axioms. : : : : : : : : : : : : : : : : : : : : : 71 4{3 Properties of the visibility relation. : : : : : : : : : : : : : : : : : : 73 4{4 Rules expressing properties of the visibility relation. : : : : : : : : : 73 4{5 Derivations using rules on the visibility relation. : : : : : : : : : : : 75 vii List of Figures viii 5{1 Translation of derivations. : : : : : : : : : : : : : : : : : : : : : : : 87 6{1 General form of G. : : : : : : : : : : : : : : : : : : : : : : : : : : : 100 6{2 Dissection of Ti. : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 103 6{3 Axioms for T, B, 4 and 5. : : : : : : : : : : : : : : : : : : : : : : : 108 6{4 Derivation of (cid:6)k (cid:3)A (cid:27) (cid:3)lA using (R ). : : : : : : : : : : : : : : : 108 (cid:30) kl 6{5 Countermodel to axiomatization of directedness. : : : : : : : : : : : 115 7{1 Modal proper reductions. : : : : : : : : : : : : : : : : : : : : : : : : 119 7{2 Modal permutative reductions. : : : : : : : : : : : : : : : : : : : : : 120 7{3 The cut-free sequent calculus L (T). : : : : : : : : : : : : : : : : 126 (cid:3)(cid:6) 7{4 Rules for the modi(cid:12)ed sequent calculus, L0 (T ;T). : : : : : : : : 126 H (cid:3)(cid:6) 7{5 Intuitionistic modal logics known to be decidable. : : : : : : : : : : 132 8{1 Counterexample to general soundness. : : : : : : : : : : : : : : : : 149 B{1 Derivations of the IK axioms using sequence pre(cid:12)xes. : : : : : : : : 200 Chapter 1 Introduction 1.1 Motivation Classical modal logics are extensions of classical logic with new operators (modal- ities) whose operation is intensional (i.e. non truth-functional). Originally, modal logics were used by philosophers to model intensional notions such as necessity, possibility, belief, knowledge, obligation, etc. However, there was a great deal of controversy amongst philosophers, some of whom doubted whether the whole enterprise was even meaningful. The consolidation of modal logic came in the late 1950s and early 1960s with the development of an intuitive semantics based on ‘possible worlds’ by Kripke (after whom the semantics is often named), Kanger and Hintikka (see, e.g., [50,47,44]). In philosophy, possible world semantics has been used in support of elaborate metaphysical arguments (see, e.g., Kripke [52]); however,thephilosophicalcontroversyovermodal logicisfar fromsettled. Yetthe developmentofpossibleworldsemanticshas enabledmodallogictoescapetoother (cid:12)elds. First, the semantics is mathematically natural. Thus the model theory of modal logic has become an interesting sub(cid:12)eld of mathematical logic in its own right (see, e.g., van Bentham [6]). Second, the semantics enabled modal logic to be applied to interesting mathematical problems such as Solovay’s Completeness Theorem [72]. Lastly, possible world models are closely related to the transition systems of computer science. This connection has led to many applications of 1