product iamge

Fixed-Point Logics on Trees [PhD Thesis]

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

Author(s): Amelie Gheerbrant
Series: ILLC Dissertation Series DS-2010-08
Publisher: University of Amsterdam
Year: 2010

Language: English
Pages: 193
City: Amsterdam

1 Introduction 1
2 Preliminaries 5
2.1 Trees as Relational Structures . . . . . . . . . . . . . . . . . . . . 5
2.1.1 Di erent 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