João Rasga - Decidability of Logical Theories and Their Combination

This series is devoted to the universal approach to logic and the development of a general theory of logics. It covers topics such as global set-ups for fundamental theorems of logic and frameworks for the study of logics, in particular logical matrices, Kripke structures, combination of logics, categorical logic, abstract proof theory, consequence operators, and algebraic logic. It includes also books with historical and philosophical discussions about the nature and scope of logic. Three types of books will appear in the series: graduate textbooks, research monographs, and volumes with contributed papers. All works are peer-reviewed to meet the highest standards of scientific literature.

More information about this series at http://www.springer.com/series/7391

This book is published under the imprint Birkhuser, www.birkhauser-science.com by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

The main objective of the book is to provide a self-contained introduction to decidability of first-order theories to graduate students of Mathematics and is equally suitable for Computer Science and Philosophy students who are interested in gaining a deeper understanding of the subject. The book is also directed to researchers that intend to get acquainted with first-order theories and their combinations. The technical material is presented in a systematic and universal way and illustrated with plenty of examples and a range of proposed exercises.

The book is organized as follows. In Chap. addresses the contemporary topic of combination of theories with the aim of obtaining preservation results in a universal way. Namely, we discuss preservation of satisfiability and decidability when combining theories by the Nelson-Oppen technique (see [2427]). The theories only share equality and are stably infinite. The book ends with an Appendix presenting a modicum of computability theory (see [2830]). The Appendix follows closely [30], namely, adopting as the computational model an abstract high-level programming language. The concepts of computable function, decidable set and listable set are defined and explored. The problem reduction technique is also discussed.