×

Extensions of first order logic. (English) Zbl 0848.03001

Cambridge Tracts in Theoretical Computer Science. 19. Cambridge: Cambridge Univ. Press. xxii, 388 p. (1996).
Various logical systems, extensions of first-order classical logic, such as, e.g., second-order logic, type theory, modal logic, dynamic logic and many-sorted logic, naturally appearing in mathematics, computer science, linguistics and philosophy, form the subject of this book. The expressive power of many-sorted first-order logic serves as a unifying context in which each of the logical systems treated in the book can be translated. This is the reason for the particular interest payed to the investigation of many-sorted logic and its relationships to the other logics.
In the first chapter, the introductory syntactical and semantical notions of standard second-order language, allowing quantification over sets and relations, are defined and some of the basic statements proved, among which are the coincidence lemma, the substitution lemma and the isomorphism theorem.
The second chapter deals with general questions of deductive systems and includes the sequent calculus formulation of second-order logic followed by corresponding soundness and incompleteness results.
The central theme of the third chapter is categoricity of second-order Peano arithmetic.
In the fourth chapter, second-order frames and general structures are introduced and their algebraic and logical concepts studied.
The fifth chapter treats type theory in detail. The semantics of frames and general structures is discussed and a proof of the equivalence of the usual definition of general structures with a proposed algebraic definition is presented. The equational presentation of the functional theory of finite types is included as well.
In chapter six, many-sorted logic is considered. The crucial reason of treating many-sorted logic is its successful use in computer science as well as in a wide range of logics as a unifier logic. In this chapter, language, syntax and semantics are studied, together with the soundness, completeness and compactness theorems. The reduction of many-sorted logic to first-order unsorted logic is described as well.
The book closes with the seventh chapter, devoted to applying many-sorted logic. The reductions of higher-order logics, propositional and first-order modal logic, and dynamic logic to many-sorted logic, and conversions of the corresponding structures into many-sorted structures are discussed.
This nice and clearly written book will be an appropriate introduction and reference to the contemporary subject of higher-order and many-sorted logics, not only for mathematicians, but for computer scientists, linguists and philosophers, too.

MSC:

03B15 Higher-order logic; type theory (MSC2010)
03-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
03F35 Second- and higher-order arithmetic and fragments
03B45 Modal logic (including the logic of norms)
03B10 Classical first-order logic
03G25 Other algebras related to logic
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
PDFBibTeX XMLCite