Extensions of First Order Logic

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.^[1] 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.^[2][1]

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.^[3][4] 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.^[1][4] Chapter four formulates a non-standard semantics for second-order logic (from Henkin),^[3] in which quantification over relations is limited to only the definable relations.^[4] 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.^[1][3] 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.^[3]