Fibring LogicsModern applications of logic, in mathematics, theoretical computer science, and linguistics, require combined systems involving many different logics working together. In this book the author offers a basic methodology for combining-or fibring-systems. This means that many existing complex systems can be broken down into simpler components, hence making them much easier to manipulate. Using this methodology the book discusses ways of obtaining a wide variety of multimodal, modal intuitionistic, modal substructural and fuzzy systems in a uniform way. It also covers self-fibred languages which allow formulae to apply to themselves. The book also studies sufficient conditions for transferring properties of the component logics into properties of the combined system. |
Contents
| 1 | |
| 18 | |
Combining modal logics | 39 |
Intuitionistic modal logics | 76 |
Discussion and comparison with the literature | 91 |
Introducing selffibring | 112 |
Selffibring of predicate logics | 124 |
Selffibring with function symbols | 148 |
Combining temporal logic systems | 255 |
Fibring implication logics | 283 |
Grafting modalities onto substructural implication systems | 307 |
Products of modal logics | 327 |
Fibring intuitionistic logic programs | 380 |
Fibring semantic tableaux | 401 |
Fibring modal tableaux | 421 |
Fibring labelled deductive systems | 440 |
Selffibring of intuitionistic logic | 158 |
Applications of selffibring | 175 |
Conditional implications and nonmonotonic consequence | 210 |
How to make your logic fuzzy | 227 |
Conclusion and discussion | 457 |
Index | 473 |
Other editions - View all
Common terms and phrases
actual world algebra applied arbitrary assignment assume atomic q axiomatisation axioms binary binary relation C₁ calculus canonical model classical logic clause completeness theorem connectives consequence relation consider consistent construction corresponding countermodel defined Definition denote disjunction dovetailed equivalent evaluation example extension F₁ fibred model fibred semantics fibring function finite first-order following holds formula frame free logic free variables function F function symbols fuzzy Gabbay generalised Hence implies intuitionistic logic Kripke frames Kripke model Kripke semantics L₁ L1 and L2 labels language Lemma logic programming logic system modal logic monadic monotonic multimodal logic n-modal non-monotonic notation notion obtained operators possible world predicate logic proof properties propositional quantifiers restricted rules satisfies Section self-fibred subset substitution substructural logics temporal logic temporalisation theory transitive translation truth value two-dimensional unary predicate valid wffs
Popular passages
Page ii - Alec Fisher: Formal number theory and computability: a work book 8. Anand Pillay: An introduction to stability theory 9. HE Rose: Subrecursion: functions and hierarchies 10. Michael Hallett: Cantorian set theory and limitation of size 11. R. Mansfield and G. Weitkamp: Recursive aspects of descriptive set theory 12. JL Bell: Boolean-valued models and independence proofs in set theory (2nd edition) 13. Melvin Fitting: Computability theory: semantics and logic programming 14. JL Bell: Toposes and local...
Page ii - Choice sequences: a chapter of intuitionistic mathematics 4. JL Bell: Boolean-valued models and independence proofs in set theory (1st edition) 5. Krister Seberberg: Classical propositional operators: an exercise in the foundation of logic 6.
Page 426 - So far we have provided definitions about the structure of the labels without regard to the elements they are made of. The following definitions will be concerned with the type of world symbols occurring in a label. Let t be a label and t...
Page 426 - The appropriate dummy label will be specified in the applications where such a notion is used. However, it can be viewed also as an independent atomic label. In the context of fibring WQ can be thought of as denoting the actual world obtained via the fibring function from the world denoted by s"(i). Example 19.5.
Page 433 - The rules for the modal operators are as usual, "m new" in the proviso for the i/i- and 7r,-rule means: m must not have occurred in any label yet used. Notice that in all inferences via an a-rule the label of the premise carries over unchanged to the conclusion, and in all inferences via a...
Page 421 - Mondadori's (1994) classical proof system KE, a combination of tableau and natural deduction inference rules which allows for a restricted ( "analytic" ) use of the cut rule. The key feature of KEM, besides its being based neither on resolution nor on standard sequent/tableau inference techniques, is that it generates models and checks them using a label scheme for bookkeeping fibred models.
Page 433 - As usual with refutation methods a K.EM-proof of A consists of a successful attempt to construct a countermodel for A by assuming that A is false in some arbitrary model, which means that we assume that A is false in the actual world of the model.
Page 45 - This assumption does not affect satisfaction in models because points not accessible from a by any power R" of R do not affect truth values at a. Moreover we assume that all sets of possible worlds in any...