Correspondence and Canonicity in Non-Classical Logic [PhD Thesis]

1 Introduction 1
1.1 Outline of chapters . . . . . . . 13
2 Sahlqvist correspondence and canonicity 17
2.1 Modal logic . . . . . . . . . 17
2.2 Correspondence . . . . . . . . . 22
2.3 Syntactic classes . . . . . . . . 23
2.4 Algorithmic strategies . . . . . . . 26
2.5 Duality and Canonicity . . . . . . . 31
3 Basic algebraic modal correspondence 33
3.1 Preliminaries . . . . . . . . . 34
3.1.1 Meaning Function . . . . . . . 34
3.1.2 Definite implications . . . . . . 35
3.2 Algebraic correspondence . . . . . . . 36
3.2.1 The general reduction strategy . . . . . 37
3.2.2 Uniform and Closed formulas . . . . . 38
3.2.3 Very simple Sahlqvist implications . . . . 40
3.2.4 Sahlqvist implications . . . . . . 44
3.3 Conclusions . . . . . . . . . 49
4 Algorithmic correspondence and canonicity for regular modal logic 51
4.1 Preliminaries . . . . . . . . . 52
4.1.1 Regular modal logics . . . . . . 53
4.1.2 Kripke frames with impossible worlds and their complex algebras . . . . . . . . . 55
4.1.3 Algebraic semantics . . . . . . . 56
4.1.4 The distributive setting . . . . . . 57
4.1.5 Canonical extension . . . . . . . 58
4.1.6 Adjoints and residuals . . . . . . 59
4.2 Algebraic-algorithmic correspondence . . . . . 61
4.2.1 The basic calculus for correspondence . . . 64
4.3 ALBA on regular BDL and HA expansions . . . . 66
4.3.1 The expanded language L+ . . . . . 66
4.3.2 The algorithm ALBAr . . . . . . 68
4.3.3 Soundness and canonicity of ALBAr . . . . 71
4.4 Sahlqvist and Inductive DLR- and HAR- inequalities . . 73
4.5 Applications to Lemmon's logics . . . . . . 78
4.5.1 Standard translation . . . . . . 79
4.5.2 Strong completeness and elementarity of E2-E5 . . 80
4.6 Conclusions . . . . . . . . . 84
5 Algorithmic correspondence for intuitionistic modal mu-calculus 87
5.1 Preliminaries . . . . . . . . . 88
5.1.1 The bi-intuitionistic modal mu-language and its semantics 88
5.1.2 Perfect modal bi-Heyting algebras . . . . 91
5.2 ALBA for bi-intuitionistic modal mu-calculus: setting the stage . . . . . . 92
5.2.1 Preservation and distribution properties of extremal fixed points . . . . . . . . . 92
5.2.2 Approximation rules and their soundness . . . 96
5.2.3 Adjunction rules and their soundness . . . 97
5.2.4 Recursive Ackermann rules . . . . . 98
5.2.5 From semantic to syntactic rules . . . . . 99
5.3 Recursive mu-inequalities . . . . . . . 99
5.3.1 Recursive mu-inequalities . . . . . 100
5.3.2 General syntactic shapes and a comparison with existing Sahlqvist-type classes . . . . . . 102
5.4 Inner formulas and their normal forms . . . . . 105
5.4.1 Inner formulas . . . . . . . 105
5.4.2 Towards syntactic adjunction rules . . . . 107
5.4.3 Normal forms and normalization . . . . . 108
5.4.4 Computing the adjoints of normal inner formulas . 111
5.5 Adjunction rules for normal inner formulas . . . . 115
5.6 Examples . . . . . . . . . 119
5.7 Conclusions . . . . . . . . . 124
6 Pseudocorrespondence and relativized canonicity 125
6.1 Preliminaries . . . . . . . . . 127
6.1.1 Language, basic axiomatization and algebraic semantics of DLE and DLE . . . . . . . 127
6.1.2 Inductive DLE and DLE inequalities . . . 128
6.2 Pseudo-correspondence and relativized canonicity and correspondence . . . . . . 130
6.3 An alternative proof of the canonicity of additivity . . 135
6.3.1 A purely order-theoretic perspective . . . . 135
6.3.2 Canonicity of the additivity of DLE-term functions . 140
6.4 Towards extended canonicity results: enhancing ALBA . . 141
6.5 Meta-inductive inequalities and success of ALBAe . . . 145
6.6 Relativized canonicity via ALBAe . . . . . 146
6.7 Examples . . . . . . . . . 147
6.8 Conclusions . . . . . . . . . 149
7 Subordinations, closed relations, and compact Hausdorff spaces151
7.1 Preliminaries . . . . . . . . . 152
7.2 Subordinations on Boolean algebras . . . . . 154
7.3 Subordinations and closed relations . . . . . 156
7.4 Subordinations, strict implications, and Jonsson-Tarski duality . 160
7.5 Modally definable subordinations and Esakia relations . . 163
7.6 Further duality results . . . . . . . 166
7.7 Lattice subordinations and the Priestley separation axiom . 169
7.8 Irreducible equivalence relations, compact Hausdorff spaces, and
de Vries duality . . . . . . . . . 171
7.9 Conclusion . . . . . . . . . 175
8 Sahlqvist preservation for topological fixed-point logic 177
8.1 Preliminaries . . . . . . . . . 179
8.2 Topological fixed-point semantics . . . . . 181
8.2.1 Open fixed-point semantics . . . . . 184
8.3 Algebraic semantics . . . . . . . 186
8.4 Sahlqvist preservation . . . . . . . 189
8.4.1 An alternative fixed-point semantics . . . 189
8.4.2 Esakia's lemma . . . . . . . 194
8.4.3 Sahlqvist formulas . . . . . . . 196
8.5 Sahlqvist correspondence . . . . . . . 197
8.6 Conclusion . . . . . . . . . 201
A Success of ALBA on inductive and recursive inequalities 203
A.1 ALBAr succeeds on inductive inequalities . . . . 203
A.2 Success on recursive -inequalities . . . . . 207
A.3 Preprocess, first approximation and approximation . . 207
A.4 Application of adjunction rules . . . . . . 210
A.5 The "-Ackermann shape . . . . . . . 211
B Topological Ackermann Lemmas 213
B.1 Intersection lemmas . . . . . . . 213
B.2 Topological Ackermann Lemma . . . . . . 216
Bibliography 219
Index 231
Samenvatting 235
Abstract 237