Fixed-Point Logics on Trees [PhD Thesis]

1 Introduction 1
2 Preliminaries 5
2.1 Trees as Relational Structures . . . . . . . . . . . . . . . . . . . . 5
2.1.1 Dierent Sorts of Trees . . . . . . . . . . . . . . . . . . . . 5
2.1.2 Fixed-Point Extensions of First-Order Logic . . . . . . . . 7
2.1.3 Expressive Power . . . . . . . . . . . . . . . . . . . . . . . 19
2.2 The Modal Logic Perspective on Trees . . . . . . . . . . . . . . . 21
2.2.1 Basic Modal Logic . . . . . . . . . . . . . . . . . . . . . . 21
2.2.2 Temporal and Fixed-Point Extensions of Basic Modal Logic 25
2.2.3 Expressive Power . . . . . . . . . . . . . . . . . . . . . . . 28
2.3 Tools and Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.3.1 Decidability . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.3.2 Complete Axiomatizations . . . . . . . . . . . . . . . . . . 34
2.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3 Complete Axiomatization of Fragments of MSO on Finite Trees 37
3.1 The Axiomatizations . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.2 Henkin Completeness . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.3 Operations on Henkin-Structures . . . . . . . . . . . . . . . . . . 48
3.3.1 Ehrenfeucht-Fraisse Games on Henkin-Structures . . . . . 54
3.3.2 Fusion Theorems on Henkin-Structures . . . . . . . . . . . 62
3.4 Putting it Together: Completeness on Finite Trees . . . . . . . . . 75
3.4.1 Forests and Operations on Forests . . . . . . . . . . . . . . 75
3.4.2 Main Proof of Completeness . . . . . . . . . . . . . . . . . 77
3.4.3 Denability of the Class of Finite Trees . . . . . . . . . . . 78
3.5 Finite Linear Orders . . . . . . . . . . . . . . . . . . . . . . . . . 79
4 Interpolation for Linear Temporal Languages 81
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
4.2.1 Abstract Temporal Languages . . . . . . . . . . . . . . . . 83
4.2.2 Propositional Linear Temporal Logic . . . . . . . . . . . . 84
4.2.3 Linear Time μ-Calculus . . . . . . . . . . . . . . . . . . . 85
4.3 Projective Denability versus Denability with Fixed-Points . . . 86
4.4 Temporal Languages with Craig Interpolation . . . . . . . . . . . 93
4.5 Interpolation Closure Results for Temporal Languages . . . . . . . 95
4.5.1 The Interpolation Closure of LTL(F) . . . . . . . . . . . . 95
4.5.2 The Interpolation Closure of LTL(F) . . . . . . . . . . . . . 97
4.6 Finite Linear Orders . . . . . . . . . . . . . . . . . . . . . . . . . 99
4.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
5 Complete Axiomatization of μTL(U) 101
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
5.2.1 Linear Time μ-Calculus . . . . . . . . . . . . . . . . . . . 102
5.2.2 Stutter-Invariance . . . . . . . . . . . . . . . . . . . . . . . 105
5.3 The Logic μTL(<>Г) . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.4 Complete Axiomatization of μTL(<>Г) . . . . . . . . . . . . . . . . 110
5.5 Complete Axiomatization of μTL(U) . . . . . . . . . . . . . . . . 112
5.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
6 Fixed-point Logics on Finite Extensive Games 117
6.1 Game Solution as Rational Procedure . . . . . . . . . . . . . . . . 117
6.2 From Functional to Relational Strategies . . . . . . . . . . . . . . 119
6.3 Dening BI as a Unique Static Relation . . . . . . . . . . . . . . . 122
6.4 A Dynamic-Epistemic Scenario: Iterated Announcement of Rationality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
6.5 Another Dynamic Scenario: Beliefs and Iterated Plausibility Upgrade129
6.6 Midway Conclusion: Dynamic Foundations . . . . . . . . . . . . . 136
6.7 Test Case: Variants of Backward Induction . . . . . . . . . . . . . 137
6.7.1 Dening BI' in Partial Fixed-Point Logic . . . . . . . . . . 137
6.7.2 Dening BI' in In
ationary Fixed-Point Logic . . . . . . . 139
6.7.3 Alternative: Recursion on Well-Founded Tree Order . . . . 140
6.8 Excursion: Order-Conform Fixed-Point Logics . . . . . . . . . . . 143
6.8.1 Order-Conform Operators . . . . . . . . . . . . . . . . . . 144
6.8.2 The Modal i-Calculus . . . . . . . . . . . . . . . . . . . . 147
6.9 TowardsWell-Behaved Fixed-Point Logics on Finite Extensive Games150
6.10 Further Issues in Extended Game Logics . . . . . . . . . . . . . . 152
6.11 Coda: Alternatives to Backward Induction and True Game Dynamics154
6.12 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156
7 Conclusion 157
Samenvatting 171
Abstract 173