Formal design and verification involve two historically disparate methods: theorem proving (syntactic proofs) [1] and model checking (semantic truth valuations) [2]. The insight and perspective to be gained from this book, on both methods, would be hard to overestimate. The perspective arises from fundamentals: “This book is to serve as a basis for ... bounded reverse mathematics ... inspired by the Friedman/Simpson program Reverse Mathematics [RM]. The goal is to find the weakest theory capable of proving a given theorem” [3]. I am pleased to be in the authors’ peripheral company with respect to RM, however accidentally I blundered into it a few years ago. RM convinces us that the 1931 reports of the death of mathematics were highly exaggerated.

This decidedly advanced research monograph is written by a Turing Award laureate and one of his former students (now colleague). A prospective PhD intending to specialize in computational complexity, proof theory, or a species of reverse mathematics will find no straighter road (albeit on a steep incline) that leads to a point of departure for further research and contribution to the field. The book is a must-read for such a person, as well as for already-accomplished researchers. But there is much in it for us nonspecialists as well. For example, a safety-critical control system in which I was involved generated 35,000 proof obligations (of the syntactic variety), most of which were discharged by computer. An ancillary system was verified via model checking, that is, semantic means (truth tables). So, the complexity of proofs and verifications, which is admittedly not the broad subject of this book, is the most practical of issues. Thus, this book comprises the best reading about the subject for people involved in applied logic and applied complexity.

A brief introductory chapter delineates the book’s subject as the detailed explication “of the three-way association among complexity classes, theories, and proof systems.” But the authors’ notion of proof complexity goes beyond the complexity of proofs in a propositional calculus, by means of extensions to arithmetic theories that are weaker than that of Peano, that is, those with bounded arithmetic. Boundedness refers to the scope of quantifiers and to induction that is limited to bounded formulas. Table 1 in this introductory chapter enumerates 15 complexity classes, the theories that the authors associate with each class, and the sections where their logic, proof theory, and complexity are treated (in chapters 5 to 9). Table 2 lists a dozen theories, their (non)theorems or open questions, and the corresponding sections of the book that expound on them.

Chapters 2 to 4--“The Predicate Calculus and the [Gentzen] System LK,” “Peano Arithmetic and Its Subsystems,” and “Two-Sorted Logic and Complexity Classes,”--can be characterized as the book’s theoretical infrastructure. The authors advise (prior or concurrent) reading of Buss’ freely available chapters [4] and doctoral thesis, Bounded Arithmetic, for two excellent reasons: to get up to speed conceptually and to understand the specific precursors on which the present book builds. Some rationale for the choice of two-sorted logic and complexity classes (chapter 4) is already given in the preface, the two sorts being natural numbers and binary (bit-) strings, the latter being the objects of interest, by virtue of their natural relation, as inputs, to Turing machines and Boolean circuits. The natural numbers are construed to remain small--they are an ancillary sort used for indexing and for expressing the size of bit-strings.

Chapters 5 and 6 treat theories and complexity classes V0, AC0, V1, and polynomial-time complexity, while chapter 7, “Propositional Translations,” reinforces the strong interest of the book in the relationship between bounded arithmetic and propositional proof systems. The complexity of proof systems is defined in terms of “families of tautologies [that] have polynomial-length proofs.” Chapter 8 deals with polynomial-time (“and beyond”) classes, and the 100-page chapter 9 with small complexity classes and their theories. I would venture to say that those of us who cut at least some of our teeth on continuum mathematics--calculus, analysis, complex variables for scalars, and matrices--will find philosophical satisfaction in the authors’ address of the Jordan curve and Hamilton-Cayley theorems in state-of-the art proof theories.

The final chapter, on proof systems, elaborates the reflection principle (RFN), alluded to in earlier chapters, which asserts (the syntactic notion of) soundness for proof systems, given the (semantic) validity of sequents under truth assignment. One of its uses is to generate axioms for theories associated with given theories. Not to be missed, even by the casual reader, is the Boolean sentence value problem (BSVP), whose simple alphabet comprises the logical constants and connectives, plus parentheses. A “Pebbler-Challenger” game is used to prove Buss’ result that BSVP is ALogTime.

This most erudite of books will stand the test of time. I will revisit it often.