Extensions of First Order Logic

Extensions of First Order Logic is a book on mathematical logic. It was written by María Manzano, and published in 1996 by the Cambridge University Press as volume 19 of their book series Cambridge Tracts in Theoretical Computer Science.

Topics

The book concerns forms of logic that go beyond first-order logic, and in particular (following the work of Leon Henkin) the project of unifying them by translating all of these extensions into a specific form of logic, many-sorted logic. Beyond many-sorted logic, its topics include second-order logic (including its incompleteness and relation with Peano arithmetic), second-order arithmetic, type theory (in relational, functional, and equational forms), modal logic, and dynamic logic.

It is organized into seven chapters. The first concerns second-order logic in its standard form, and it proves several foundational results for this logic. The second chapter introduces the sequent calculus, a method of making sound deductions in second-order logic, and its incompleteness. The third continues the topic of second-order logic, showing how to formulate Peano arithmetic in it, and using Gödel's first incompleteness theorem to provide a second proof of incompleteness of second-order logic. Chapter four formulates a non-standard semantics for second-order logic (from Henkin), in which quantification over relations is limited to only the definable relations. It defines this semantics in terms of "second-order frames" and "general structures", constructions that will be used to formulate second-order concepts within many-sorted logic. In the fifth chapter, the same concepts are used to give a non-standard semantics to type theory. After these chapters on other types of logic, the final two chapters introduce many-sorted logic, prove its soundness, completeness, and compactness, and describe how to translate the other forms of logic into it.

Audience and reception

Although the book is intended as a textbook for advanced undergraduates or beginning graduate students, reviewer Mohamed Amer suggests that it does not have enough exercises to support a course in its subject, and that some of its proofs are lacking in detail. Reviewer Hans Jürgen Ohlbach suggests that it would be more usable as a reference than a textbook, and states that "it is certainly not suitable for undergraduates".

Reviewer Yde Venema wonders how much of the logical power and useful properties of the various systems treated in this book have been lost in the translation to many-sorted logic, worries about the jump in computational complexity of automated theorem proving caused by the translation, complains about the book's clarity of exposition becoming lost in case analysis, and was disappointed at the lack of coverage of Montague grammar, fixed-point logic, and non-monotonic logic. Nevertheless, Venema recommends the book for courses introducing students to second-order and many-sorted logics, praising the book for its "overwhelming and catching enthusiasm". And reviewer B. Boričić calls it "nice and clearly written", "an appropriate introduction and reference", recommending it to researchers in several disciplines (mathematics, computer science, linguistics, and philosophy) where advanced forms of logic are important.