Hybrid Logic and its Proof-TheoryThis 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). |
Contents
| 1 | |
2 ProofTheory of Propositional Hybrid Logic | 21 |
3 Tableaus and Decision Procedures for Hybrid Logic | 59 |
4 Comparison to Seligmans Natural Deduction System | 91 |
5 Functional Completeness for a Hybrid Logic | 108 |
6 FirstOrder Hybrid Logic | 127 |
7 Intensional FirstOrder Hybrid Logic | 153 |
8 Intuitionistic Hybrid Logic | 171 |
9 Labelled Versus Internalized Natural Deduction | 202 |
10 Why Does the ProofTheory of Hybrid Logic Behave So Well? | 211 |
| 221 | |
| 229 | |
Other editions - View all
Common terms and phrases
accessibility applied assignment Assume axiom system binder Bra¨uner branch called chapter classical clause completeness conclusion connective consider contains corresponding defined Definition derivation designators discharged discussion element elimination rules equivalence example exists expressive extended Figure finite first-order hybrid logic first-order logic follows formula occurrence function Gentzen system give given hence hybrid-logical implies induction instance intension intensional interpretation introduction introduction rule involving labelled language Lemma modal logic Moreover namely natural deduction system NH(O nominal normal Note object obtained occur ordinary permutable predicate premise present Proof propositional propositional symbol prove range reasoning reduction rules relation replaced respect result satisfaction statements satisfy says schemas Section semantics sense sequent similar sound standard straightforward stubborn subformula tableau system Theorem tion translation true undischarged assumptions valid