Braüner Hybrid Logic and its Proof-Theory

1. Auflage 2010
ISBN: 978-94-007-0002-4
Verlag: Springer Netherlands
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 37, 240 Seiten

Reihe: Applied Logic Series

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.

Autoren/Hrsg.

Braüner, Torben

Inhaltsverzeichnis

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