Modal Logics of Ordered Trees [PhD Thesis]

1 Zooming in 1
1.1 Adding a Zoom to Linear Temporal Logic . . . . . . . . . . . . . . . . . . 1
1.2 Thesis Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2 Modal and Temporal Logics 13
2.1 Introducing Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Possible World Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3 Axioms and Correspondences . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.4 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.5 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3 Semantic Characterisation 39
3.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.2 Some Defined Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.3 Correspondences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.4 Ontological Considerations . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.5 General Models and P-morphisms . . . . . . . . . . . . . . . . . . . . . . 60
3.6 Loosely Ordered Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
3.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
4 Axiomatic Characterisation 97
4.1 Axioms and Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
4.2 Some Derived Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
4.3 Completeness without Descendant Modalities . . . . . . . . . . . . . . . . 113
4.4 Alternatives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
5 Decidability 147
5.1 Monadic Second-order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 147
5.2 Finite Binary Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159
5.3 Discretely Ordered Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
5.4 General Ordered Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
5.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182
6 Zooming out 185
6.1 Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
6.2 Summary of Main Results . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
6.3 Open Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
Appendices 197
A Relations and Orders 199
A.1 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199
A.2 Linear Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200
B Derivations 203
B.1 Proof of Lemma 4.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203
Bibliography 205
List of Figures 211
List of Tables 213
Index 215