Hybrid Logic and its Proof-Theory

Preface

Contents

1 Introduction to Hybrid Logic

1.1 Informal Motivation

1.2 Formal Syntax and Semantics

1.2.1 Translation into First-Order Logic

1.3 The Origin of Hybrid Logic in Prior's Work

1.3.1 Did Prior Reach His Philosophical Goal?

1.4 The Development Since Prior

2 Proof-Theory of Propositional Hybrid Logic

2.1 The Basics of Natural Deduction Systems

2.2 Natural Deduction for Propositional Hybrid Logic

2.2.1 Conditions on the Accessibility Relation

2.2.2 Some Admissible Rules

2.2.3 Soundness and Completeness

2.2.4 Normalization

2.2.5 The Form of Normal Derivations

2.2.6 Discussion

2.3 The Basics of Gentzen Systems

2.4 Gentzen Systems for Propositional Hybrid Logic

2.4.1 Soundness and Completeness

2.4.2 The Form of Derivations

2.4.3 Discussion

2.5 Axiom Systems for Propositional Hybrid Logic

2.5.1 Soundness and Completeness

2.5.2 Discussion

3 Tableaus and Decision Procedures for Hybrid Logic

3.1 The Basics of Tableau Systems

3.2 A tableau System Including the Universal Modality

3.2.1 Tableau Rules for Hybrid Logic

3.2.2 Some Properties of the Tableau System

3.2.3 Systematic Tableau Construction

3.2.4 The Model Existence Theorem and Decidability

3.2.5 Tableau Examples

3.3 A Tableau System Not Including the Universal Modality

3.3.1 A Hybrid-Logical Version of Analytic Cuts

3.4 The Tableau Systems Reformulated as Gentzen Systems

3.5 Discussion

4 Comparison to Seligman's Natural Deduction System

4.1 The Natural Deduction Systems Under Consideration

4.1.1 Seligman's Original System

4.2 Translation from Seligman-Style Derivations

4.3 Translation to Seligman-Style Derivations

4.4 Reduction Rules

4.5 Discussion

5 Functional Completeness for a Hybrid Logic

5.1 The Natural Deduction System Under Consideration

5.2 Introduction to Functional Completeness

5.3 The General Rule Schemas

5.3.1 Earlier Work on Functional Completeness

5.3.2 Rule Schemas for Hybrid Logic

5.3.3 Normalization and Conservativity

5.4 Functional Completeness

5.5 Discussion

6 First-Order Hybrid Logic

6.1 Introduction to First-Order Hybrid Logic

6.1.1 Some Remarks on Existence and Quantification

6.1.2 Rigidified Constants

6.1.3 Translation into Two-Sorted First-Order Logic

6.2 Natural Deduction for First-Order Hybrid Logic

6.2.1 Conditions on the Accessibility Relation

6.2.2 Some Admissible Rules

6.2.3 Soundness and Completeness

6.2.4 Normalization

6.2.5 The Form of Normal Derivations

6.3 Axiom Systems for First-Order Hybrid Logic

7 Intensional First-Order Hybrid Logic

7.1 Introduction to Intensional First-Order Hybrid Logic

7.1.1 Generalized Models

7.1.2 Translation into Three-Sorted First-Order Logic

7.2 Natural Deduction for Intensional First-Order Hybrid Logic

7.2.1 Soundness and Completeness: Generalized Models

7.2.2 Soundness and Completeness: Standard Models

7.3 Partial Intensions

8 Intuitionistic Hybrid Logic

8.1 Introduction to Intuitionistic Hybrid Logic

8.1.1 Relation to Many-Valued Semantics

8.1.2 Relation to Birelational Semantics

8.1.3 Translation into Intuitionistic First-Order Logic

8.2 Natural Deduction for Intuitionistic Hybrid Logic

8.2.1 Conditions on the Accessibility Relation

8.2.2 An Admissible Rule

8.2.3 Soundness and Completeness

8.2.4 Normalization

8.2.5 The Form of Normal Derivations

8.3 Axiom Systems for Intuitionistic Hybrid Logic

8.4 Axiom Systems for a Paraconsistent Hybrid Logic

8.4.1 Soundness and Completeness

8.5 A Curry-Howard Interpretation of Intuitionistic Hybrid Logic

9 Labelled Versus Internalized Natural Deduction

9.1 A Labelled Natural Deduction System for Modal Logic

9.2 The Internalization Translation

9.3 Reductions

9.4 Comparison of Reductions

9.4.1 A Remark on Normalization

10 Why Does the Proof-Theory of Hybrid Logic Behave So Well?

10.1 The Success Criteria

10.1.1 Standard Systems for Modal Logic

10.1.2 Labelled Systems for Modal Logic

10.2 Why Hybrid-Logical Proof-Theory Behaves So Well

10.3 Comparison to Internalization of Bivalent Semantics

10.4 Some Concluding Philosophical Remarks

References

Index