This is a high-level textbook suitable for very bright undergraduate mathematics majors and sophisticated graduate students. The first three- fifths of the book deal with propositional and first-order logic, and the rest with type theory. In the course of a standard development of logic, the author also includes a proof of J. A. Robinson’s Resolution Theorem for propositional logic, a treatment of first-order completeness through Smullyan’s Unifying Principle (in addition to a regular Henkin-style proof), natural deduction and Gentzen-style systems, semantic tableaux (a pedagogical disaster), Herbrand’s Theorem, J. A. Robinson’s Unification Theorem, Craig’s Interpolation Theorem, and Beth’s Definability Theorem. Type theory is based on a modification of L. Henkin’s variant [Fundam. Math. 52, 323-344 (1963; Zbl 0127.006)] of A. Church’s formulation [J. Symb. Logic 5, 56-68 (1940; Zbl 0023.28901)]. The emphasis is not on set-theoretic aspects but on incompleteness and undecidability results (recursive functions, Gödel’s theorems, the Gödel-Rosser Theorem, Tarski’s Theorem). The exposition here is rather Spartan but very neat and well-designed.
The author claims that ”axiomatic set theory is more popular with mathematicians [than type theory] simply because it is much better known” and that this is an ”accident of intellectual history”. He rightly points out that the distinctions made in type theory between different types of objects are ”already implicit in mathematical practice”. However, the reviewer feels that the popularity of axiomatic set theory may be due to other factors as well, in particular to the absence of a cumbersome type notation and to the ease with which it can be translated into ordinary language. This book gives the readers a chance to weigh for themselves the advantages of type theory versus those of axiomatic set theory.