Analysis and synthesis of logics. How to cut and paste reasoning systems (Q2469685)

The project of combination of logics, started by professor Dov M. Gabbay and his collaborators during the last years of the twentieth century [see \textit{D. M. Gabbay}, ``Fibred semantics and the weaving of logics. I'', J. Symb. Log. 61, No. 4, 1057--1120 (1996; Zbl 0872.03007), ``An overview of fibred semantics and the combination of logics'', in: F. Baader et al. (eds.), Frontiers of combining systems. First international workshop, Munich, Germany, March 26--29, 1996. Dordrecht: Kluwer Academic Publishers. Appl. Log. Ser. 3, 1--55 (1996; Zbl 0896.03009), Fibring logics. Oxford Logic Guides. 38. Oxford: Clarendon Press (1999; Zbl 0909.03001)], enters now, through the book under review, the phase of becoming a dominant and very propulsive project of contemporary logic applications. This book develops some basic ideas and methods that could help logicians, computer scientists and philosophers to have access to the general, but yet elementary, mathematical theory of combining and decomposing logics, bringing together sample results, problems and perspectives, and involving the idea of cutting and pasting logics. By quoting the most important facts, chapter by chapter, we proceed with this review. In the introductory overview, Chapter 1, consequence systems, as an abstract way to present logics via a consequence operator, are described, followed by the basic ideas of composing and decomposing logics, as minimal and maximal constructions. It becomes obvious here that the pursuit for combining logics is dictated by both philosophical and by practical reasons. In the second chapter, the authors use the context of propositional language in order to investigate the concept of fibring in a homogeneous setting where both component logics are presented as Hilbert type systems. The central point are the syntactic preservation results, including the metatheorems of the \textit{modus ponens}, deduction and congruence, as well as the preservation of the interpolation property. The third chapter concentrates on the semantic aspects of logics and their fibrings. Preservation of some semantical properties by fibring, such as soundness and completeness, on the basis of an ordered algebraic interpretation structure, is studied. To illustrate these concepts, the authors use classical, modal (K, S4 and B), intuitionistic and 3-valued Gödel and Łukasiewicz logics. It is also discussed how algebraic fibring captures fibring by functions. Chapter 4 deals with heterogeneous fibring, i.e. with the fibring of logics when (i) one is presented in a semantic way (for instance, by a satisfaction system) and the other is presented by a (Hilbert, sequent or tableau) calculus; (ii) both are presented by calculi, but these are of different nature, or (iii) both are presented by different semantic structures. The notion of abstract proof system, as the adequate setting for speaking about derivations, is introduced here. The fibring techniques presented in the introductory chapters are extended to non-truth functional logics in Chapter 5. These considerations include some examples of conditional equational logics and paraconsistent modal logics. Chapter 6 addresses the problem of fibring the first-order language based logics. To deal with the problem of substitution of a schema variable within the scope of quantifiers the notion of inference rule with proviso is introduced, ensuring a safe use of substitutions when the corresponding inference rule is applied in a derivation. Chapter 7 defines a wide class of higher-order logics equipped with topos semantics and with Hilbert calculi, making a more convenient way to present the corresponding notions of fibring as categorical constructions. It is shown that the basic example of higher-order logic, the Hilbert type axiomatization of intuitionistic logic, is sound with respect to a slightly generalized notion of topos semantics. There is also established a general completeness result: every full logic system with Hilbert calculus, including higher-order logics, and enjoying the metatheorem of deduction, is complete. Chapter 8 describes a solution to the collapsing problem in the context of propositional language based logics, both for global and local reasoning. The method used here is the modulated fibring, which is very close to the notion of fibring by functions. This concept is illustrated by examples including classical, intuitionistic, \(3\)-valued Gödel and Łukasiewicz propositional logics. Chapter 9 deals with the problem of splitting logics, emphasizing the role of possible-translations semantics and contrasting with the previous chapters that consider the forms of splicing. The second semantical method for splitting logics analyzed here is the direct union of matrices and the related plain fibring. The new tendencies on fibring are discussed in Chapter 10, including the network fibring using a labelled formulation of modal logics, as well as the recursive Bayesian networks. The last chapter presents a summing-up of the different techniques for combining logics included in this book together with their main features. It also includes an outlook at new research directions in both the existing combination mechanisms and also new forms of combinations. The techniques developed here will be useful in the fields of computational linguistics, automated reasoning, complexity, artificial intelligence, software specification, knowledge representation, security protocols and authentication, cryptography, temporal, epistemic and probabilistic logics etc. The book will be of interest to researchers and graduate students in mathematical logic, theory of computation and philosophical logic with no previous knowledge of combining and decomposing logics, but with a working knowledge of the subject of first-order logic. This will be one more jewel in Springer's Applied Logic Series.