Hybrid Logic and its Proof-Theory (eBook)

Torben Braüner (Autor)

eBook Download: PDF

2010 | 2011
XIII, 231 Seiten
Springer Netherland (Verlag)
978-94-007-0002-4 (ISBN)

Infos

This book is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model. The extra expressive power is useful for many applications, for example, when reasoning about time one often wants to formulate a series of statements about what happens at specific times. There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems for different modal logics are often unclear. The present book demonstrates that hybrid-logical proof-theory remedies this lack of uniformity in ordinary modal-logical proof systems. It considers a spectrum of different versions of hybrid logic (propositional, first-order, international first-order, and intuitionist) and of different types of proof-systems for hybrid-logic (natural deduction, Gentzen, tableaux, and axiom systems). All these systems can be motivated independently, but the fact that the systems can be given in a uniform way shows that hybrid logic and hybrid-logical proof theory is a natural enterprise.

---

This is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model (where the points represent times, possible worlds, states in a computer, or something else). This is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times. There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems for different modal logics are often unclear. In the present book we demonstrate that hybrid-logical proof-theory remedies these deficiencies by giving a spectrum of well-behaved proof systems (natural deduction, Gentzen, tableau, and axiom systems) for a spectrum of different hybrid logics (propositional, first-order, intensional first-order, and intuitionistic).

Inhalt

Preface 6
Contents 11
1 Introduction to Hybrid Logic 14
1.1 Informal Motivation 14
1.2 Formal Syntax and Semantics 18
1.2.1 Translation into First-Order Logic 20
1.3 The Origin of Hybrid Logic in Prior's Work 23
1.3.1 Did Prior Reach His Philosophical Goal? 27
1.4 The Development Since Prior 29
2 Proof-Theory of Propositional Hybrid Logic 34
2.1 The Basics of Natural Deduction Systems 34
2.2 Natural Deduction for Propositional Hybrid Logic 38
2.2.1 Conditions on the Accessibility Relation 41
2.2.2 Some Admissible Rules 43
2.2.3 Soundness and Completeness 45
2.2.4 Normalization 50
2.2.5 The Form of Normal Derivations 56
2.2.6 Discussion 59
2.3 The Basics of Gentzen Systems 61
2.4 Gentzen Systems for Propositional Hybrid Logic 63
2.4.1 Soundness and Completeness 64
2.4.2 The Form of Derivations 66
2.4.3 Discussion 66
2.5 Axiom Systems for Propositional Hybrid Logic 67
2.5.1 Soundness and Completeness 69
2.5.2 Discussion 70
3 Tableaus and Decision Procedures for Hybrid Logic 71
3.1 The Basics of Tableau Systems 71
3.2 A tableau System Including the Universal Modality 74
3.2.1 Tableau Rules for Hybrid Logic 74
3.2.2 Some Properties of the Tableau System 76
3.2.3 Systematic Tableau Construction 78
3.2.4 The Model Existence Theorem and Decidability 80
3.2.5 Tableau Examples 83
3.3 A Tableau System Not Including the Universal Modality 88
3.3.1 A Hybrid-Logical Version of Analytic Cuts 92
3.4 The Tableau Systems Reformulated as Gentzen Systems 95
3.5 Discussion 100
4 Comparison to Seligman's Natural Deduction System 103
4.1 The Natural Deduction Systems Under Consideration 103
4.1.1 Seligman's Original System 105
4.2 Translation from Seligman-Style Derivations 107
4.3 Translation to Seligman-Style Derivations 109
4.4 Reduction Rules 113
4.5 Discussion 118
5 Functional Completeness for a Hybrid Logic 120
5.1 The Natural Deduction System Under Consideration 120
5.2 Introduction to Functional Completeness 123
5.3 The General Rule Schemas 124
5.3.1 Earlier Work on Functional Completeness 124
5.3.2 Rule Schemas for Hybrid Logic 128
5.3.3 Normalization and Conservativity 130
5.4 Functional Completeness 132
5.5 Discussion 136
6 First-Order Hybrid Logic 138
6.1 Introduction to First-Order Hybrid Logic 138
6.1.1 Some Remarks on Existence and Quantification 142
6.1.2 Rigidified Constants 143
6.1.3 Translation into Two-Sorted First-Order Logic 146
6.2 Natural Deduction for First-Order Hybrid Logic 149
6.2.1 Conditions on the Accessibility Relation 150
6.2.2 Some Admissible Rules 153
6.2.3 Soundness and Completeness 154
6.2.4 Normalization 158
6.2.5 The Form of Normal Derivations 160
6.3 Axiom Systems for First-Order Hybrid Logic 161
7 Intensional First-Order Hybrid Logic 164
7.1 Introduction to Intensional First-Order Hybrid Logic 164
7.1.1 Generalized Models 168
7.1.2 Translation into Three-Sorted First-Order Logic 171
7.2 Natural Deduction for Intensional First-Order Hybrid Logic 174
7.2.1 Soundness and Completeness: Generalized Models 175
7.2.2 Soundness and Completeness: Standard Models 177
7.3 Partial Intensions 179
8 Intuitionistic Hybrid Logic 181
8.1 Introduction to Intuitionistic Hybrid Logic 181
8.1.1 Relation to Many-Valued Semantics 185
8.1.2 Relation to Birelational Semantics 187
8.1.3 Translation into Intuitionistic First-Order Logic 188
8.2 Natural Deduction for Intuitionistic Hybrid Logic 190
8.2.1 Conditions on the Accessibility Relation 190
8.2.2 An Admissible Rule 193
8.2.3 Soundness and Completeness 193
8.2.4 Normalization 196
8.2.5 The Form of Normal Derivations 201
8.3 Axiom Systems for Intuitionistic Hybrid Logic 204
8.4 Axiom Systems for a Paraconsistent Hybrid Logic 205
8.4.1 Soundness and Completeness 208
8.5 A Curry-Howard Interpretation of Intuitionistic Hybrid Logic 210
9 Labelled Versus Internalized Natural Deduction 212
9.1 A Labelled Natural Deduction System for Modal Logic 212
9.2 The Internalization Translation 213
9.3 Reductions 214
9.4 Comparison of Reductions 216
9.4.1 A Remark on Normalization 218
10 Why Does the Proof-Theory of Hybrid Logic Behave So Well? 220
10.1 The Success Criteria 220
10.1.1 Standard Systems for Modal Logic 222
10.1.2 Labelled Systems for Modal Logic 222
10.2 Why Hybrid-Logical Proof-Theory Behaves So Well 223
10.3 Comparison to Internalization of Bivalent Semantics 226
10.4 Some Concluding Philosophical Remarks 228
References 230
Index 238

Produkt-Details

• Erscheint lt. Verlag: 17.11.2010
• Reihe/Serie: Applied Logic Series
• Reihe/Serie: Applied Logic Series
• Zusatzinfo: XIII, 231 p.
• Verlagsort: Dordrecht
• Sprache: englisch
• Themenwelt: Geisteswissenschaften ► Philosophie ► Allgemeines / Lexika
• Themenwelt: Geisteswissenschaften ► Philosophie ► Logik
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Mathematik / Informatik ► Mathematik ► Allgemeines / Lexika
• Themenwelt: Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
• Themenwelt: Technik
• Schlagworte: Computational Logic • Logic • Mathematical Logic • Philosophical Logic
• ISBN-10: 94-007-0002-4 / 9400700024
• ISBN-13: 978-94-007-0002-4 / 9789400700024