Model Theory for Extended Modal Languages [PhD Thesis]

This is a PhD Thesis written under supervision of Prof.dr. J.A.G. Groenendijk and Prof.dr. J.F.A.K. van Benthem at the Institute for Logic, Language and Computation. 1 Introduction 1 1.1 Generalized correspondence theory . . . . . . . . . . . . . . . . . 1 1.2 Hybrid logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Overview of the thesis . . . . . . . . . . . . . . . . . . . . . . . . 4 2 Modal logic 7 2.1 Syntax and semantics . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Bisimulations and expressivity on models . . . . . . . . . . . . . . 8 2.3 Frame definability . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.4 Completeness via general frames . . . . . . . . . . . . . . . . . . . 17 2.5 Interpolation and Beth definability . . . . . . . . . . . . . . . . . 21 2.6 Decidability and complexity . . . . . . . . . . . . . . . . . . . . . 29 I Hybrid logics 35 3 Introduction to hybrid languages 37 3.1 Syntax and semantics of H, H(@) and H(E) . . . . . . . . . . . . 37 3.2 First-order correspondence languages . . . . . . . . . . . . . . . . 39 3.3 Syntactic normal forms for hybrid formulas . . . . . . . . . . . . . 40 4 Expressivity and definability 45 4.1 Bisimulations and expressivity on models . . . . . . . . . . . . . . 47 4.2 Operations on frames and formulas they preserve . . . . . . . . . 49 4.3 Frame definability . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.4 Frame definability by pure formulas . . . . . . . . . . . . . . . . . 60 4.5 Which classes definable in hybrid logic are elementary? . . . . . . 66 5 Axiomatizations and completeness 69 5.1 The axiomatizations . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.2 General frames for hybrid logic . . . . . . . . . . . . . . . . . . . 73 5.3 Completeness with respect to general frames . . . . . . . . . . . . 78 5.4 Completeness with respect to Kripke frames . . . . . . . . . . . . 87 5.5 On the status of the non-orthodox rules . . . . . . . . . . . . . . . 89 6 Interpolation and Beth definability 93 6.1 Motivations for studying interpolation . . . . . . . . . . . . . . . 94 6.2 Interpolation over proposition letters and the Beth property . . . 95 6.3 Interpolation over nominals . . . . . . . . . . . . . . . . . . . . . 100 6.4 Repairing interpolation . . . . . . . . . . . . . . . . . . . . . . . . 102 7 Translations from hybrid to modal logics 107 7.1 From H(E) to M(E) . . . . . . . . . . . . . . . . . . . . . . . . . 107 7.2 From H to M in case of a master modality . . . . . . . . . . . . . 109 7.3 From H(@) to M in case of a master modality . . . . . . . . . . . 111 7.4 From H to M in case of shallow axioms . . . . . . . . . . . . . . 113 7.5 From H(@) to M in case of shallow axioms . . . . . . . . . . . . 116 8 Transfer 119 8.1 Negative results . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 8.2 Positive results for logics admitting filtration . . . . . . . . . . . . 122 II More expressive languages 131 9 The bounded fragment and H(@, ↓) 133 9.1 Syntax and semantics . . . . . . . . . . . . . . . . . . . . . . . . . 134 9.2 Expressivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 9.3 Frame definability . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 9.4 Axiomatizations and completeness . . . . . . . . . . . . . . . . . . 142 9.5 Interpolation and Beth definability . . . . . . . . . . . . . . . . . 147 9.6 Decidability and complexity . . . . . . . . . . . . . . . . . . . . . 149 10 Guarded fragments 157 10.1 Normal forms for (loosely) guarded formulas . . . . . . . . . . . . 158 10.2 Eliminating constants . . . . . . . . . . . . . . . . . . . . . . . . . 162 10.3 Connections with hybrid logic, and interpolation . . . . . . . . . . 164 10.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166 11 Relation algebra and M(D) 167 11.1 M(D) and its relation to H(E) . . . . . . . . . . . . . . . . . . . . 168 11.2 Repairing interpolation for M(D) . . . . . . . . . . . . . . . . . . 170 11.3 An application to relation algebra . . . . . . . . . . . . . . . . . . 173 12 Second order propositional modal logic 177 13 Conclusions 183 A Basics of model theory 185 B Basics of computability theory 191 Bibliography 197 Samenvatting 205 Abstract 207