Modalities Through the Looking Glass [PhD Thesis]

1 Introduction 1
1.1 Coalgebras and Systems . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Coalgebras and Modal Logics . . . . . . . . . . . . . . . . . . . . 3
1.2.1 Basic modal logic & coalgebras . . . . . . . . . . . . . . . 4
1.2.2 Moss logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2.3 Modal logics for coalgebras . . . . . . . . . . . . . . . . . . 6
1.2.4 From modalities to functors . . . . . . . . . . . . . . . . . 7
1.3 Outline and contributions of this thesis . . . . . . . . . . . . . . . 8
2 Algebras & Coalgebras 13
2.1 Coalgebras and Algebras . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 More on Universal Coalgebra... . . . . . . . . . . . . . . . . . . . 18
2.3 Algebras, algebraic signatures, and functors . . . . . . . . . . . . 23
2.3.1 Algebraic signatures as functors . . . . . . . . . . . . . . . 23
2.3.2 Varieties . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.3.3 Monads and Algebras . . . . . . . . . . . . . . . . . . . . . 28
2.4 A first glance at logics for coalgebras . . . . . . . . . . . . . . . . 31
2.4.1 Probabilistic modal logic & coalgebras . . . . . . . . . . . 31
2.4.2 Propositional dynamic logic & coalgebras . . . . . . . . . . 32
2.4.3 Non-normal modal logic . . . . . . . . . . . . . . . . . . . 33
2.4.4 Translations . . . . . . . . . . . . . . . . . . . . . . . . . . 34
I Modalities in the Stone age 35
3 Coalgebraic Modal Logics 37
3.1 Concrete Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.2 The abstract functorial framework . . . . . . . . . . . . . . . . . . 43
3.2.1 Modal Signatures as functors on BA . . . . . . . . . . . . . 46
3.2.2 Coalgebraic modal logics beyond BA . . . . . . . . . . . . 49
3.2.3 Other features of the functorial framework . . . . . . . . . 52
3.3 Two generic coalgebraic modal logics . . . . . . . . . . . . . . . . 57
3.3.1 Moss Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.3.2 Logics of Predicate Liftings . . . . . . . . . . . . . . . . . 61
4 Comparing Coalgebraic Modal Logics 67
4.1 One step translations . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.2 Decomposing predicate liftings . . . . . . . . . . . . . . . . . . . . 74
4.2.1 Singleton Liftings . . . . . . . . . . . . . . . . . . . . . . . 76
4.2.2 Translators, Singletons and Inductive Presentations . . . . 81
4.3 Logical Translators . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.4 The Boolean Paradise . . . . . . . . . . . . . . . . . . . . . . . . 88
4.4.1 Translating predicate liftings . . . . . . . . . . . . . . . . . 89
4.4.2 Translating Moss logic . . . . . . . . . . . . . . . . . . . . 93
4.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5 From Abstract to Concrete 95
5.1 Presentations of functors . . . . . . . . . . . . . . . . . . . . . . . 95
5.1.1 Moss Liftings . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.2 Concrete logics from abstract logics . . . . . . . . . . . . . . . . . 105
5.2.1 The first representation Theorem . . . . . . . . . . . . . . 105
5.2.2 Presentations of functors on categories of algebras . . . . . 108
5.2.3 The second representation Theorem . . . . . . . . . . . . . 114
5.3 Equational coalgebraic logic . . . . . . . . . . . . . . . . . . . . . 116
5.3.1 An equational proof system for KT . . . . . . . . . . . . . 116
5.3.2 Well-based presentations . . . . . . . . . . . . . . . . . . . 119
5.3.3 A completeness proof . . . . . . . . . . . . . . . . . . . . . 124
5.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
II Coalgebraic Modal Logics at Work 135
6 Describing Behavioural Equivalence: three sides of one coin 137
6.1 An elementary construction of final coalgebras . . . . . . . . . . . 139
6.2 Behaviour & Congruences . . . . . . . . . . . . . . . . . . . . . . 150
6.3 Logical Congruences & Weak Finality . . . . . . . . . . . . . . . . 157
6.4 Different faces of the Hennessy-Milner property . . . . . . . . . . 159
6.5 Beyond sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
6.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168
7 Dynamic Modalities and Coalgebraic Logics 171
7.1 Labelling predicate liftings . . . . . . . . . . . . . . . . . . . . . . 172
7.2 More on Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . 173
7.3 Algebraic structures over labels . . . . . . . . . . . . . . . . . . . 177
7.3.1 Sequential composition . . . . . . . . . . . . . . . . . . . . 180
7.3.2 Pointwise extensions . . . . . . . . . . . . . . . . . . . . . 184
7.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
8 Fixed Points Coalgebraically 195
8.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196
8.2 Automata via Predicate liftings . . . . . . . . . . . . . . . . . . . 199
8.3 Bounded model Property . . . . . . . . . . . . . . . . . . . . . . . 201
8.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209
9 Beyond the Stone Age 211
A Some definitions from Category Theory 215
A.1 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
Bibliography 219
Index 229
Samenvatting 233
Abstract 235