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.
Author(s): Balder ten Cate
Series: ILLC Dissertation Series DS-2005-01
Publisher: University of Amsterdam
Year: 2005
Language: English
Pages: 221
City: Amsterdam
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
