This authoritative volume on computational complexity of logical systems provides a sound background in logic for computer science and mathematics students. It covers a series of complexity classes, from the basic class whose components are computed by polynomial-size families of bounded-depth circuits to the polynomial hierarchy, PH. As the authors state, “The goal is to find the weakest theory capable of proving a given theorem.” That is, the book should serve as a sufficient basis for developing a suitable framework, in the quest of identifying the smallest complexity class whose concepts are sufficient for proving a given theorem.

The fundamental problem of complexity theory is the relation of deterministic and nondeterministic computations--that is, whether P equals NP, and whether the polynomial-time hierarchy collapses. This P versus NP problem is often regarded as one of the most important open problems in contemporary mathematics. Bounded arithmetic and propositional logic are closely interrelated, and they have several explicit and implicit connections to the computational complexity theory around the P and NP question.

From the point of view of computational complexity theory, the main question surrounding bounded arithmetic is whether it is a finitely axiomatizable theory--in other words, is there a model of the theory in which the polynomial-time hierarchy does not collapse? Also, the central problem of propositional logic is whether there exists a proof system in which every tautology has a proof-of-size polynomial in the size of the tautology. This question is equivalent to asking whether the class NP is closed under complementation.

The book consists of ten chapters and an appendix. The introductory chapter presents basic concepts and results concerning proof complexity and briefly introduces the topics treated in the subsequent chapters. The second chapter presents the logical foundations for the theories of propositional and predicate calculi, together with the sequent proof systems PK and LK. Sections 2.2.5 and 2.4 provide soundness and completeness results, and some of their corollaries, for the LK system. The final section of the chapter presents Herbrand’s theorem, a complete method for proving the unsatisfiability of sets of universal formulas.

The third chapter is devoted to Peano arithmetic and its subsystems IOPEN, I&Dgr;₀, and I&Sgr;₁, where the induction scheme is restricted so that &PHgr; is OPEN, &Dgr;₀, and &Sgr;₁, respectively. A series of conservative extensions and the linear time hierarchy of I&Dgr;₀ are presented in the final sections of the chapter. In order to obtain theories that are able to capture complexity classes defined in terms of Turing machines or Boolean circuits, the authors introduce a two-sorted first-order logic as an extension of the single-sorted first-order logic previously taken into account. The basics of the two-sorted first-order logic and two-sorted complexity classes are presented next. In the final sections of chapter 4, the sequent system LK is extended to a system LK² for a two-sorted vocabulary, together with a brief discussion of the extensions of the compactness theorem and Herbrand’s theorem in the framework of two-sorted logic.

Chapter 5 introduces the theory V⁰ corresponding to AC⁰, the smallest theory considered in the hierarchy, the main result of this chapter being that V⁰ characterizes AC⁰ in the sense that the provably total functions in V⁰ are the functions of AC⁰. The witnessing theorem and the finite axiomatizability of V⁰ are provided in final sections of the chapter. The theoretical interest in the theory V¹, the two-sorted version of Buss’ theory S₂¹, stems from the fact that all polynomial-time algorithms can be described and the proofs of most of their important properties can be formalized in the framework of this theory. The main result of chapter 6 is that the theory V¹ characterizes P, similarly to the way V⁰ characterizes AC⁰. A witnessing theorem for V¹ is proved in the final section of this chapter. Chapter 7 introduces propositional translations that translate bounded predicate formulas to families of quantified Boolean formulas. A finitely axiomatizable minimal theory for polynomial time over a standard two-sorted vocabulary is presented in chapter 8.

In chapter 9, the authors propose an original uniform method to introduce minimal theories for a series of complexity classes; for each class C, its minimal theory VC is axiomatized by the axioms of V⁰, and a single axiom asserts the existence of a solution for a complete problem of C. Sections 9.2 and 9.3 present a method for developing finitely axiomatizable theories for certain uniform subclasses of P, in a similar way to VP theories for TC⁰, the smallest class that contains problems such as sorting, integer multiplications, and division, when the input integer arguments are given in binary. The final chapter of the book is devoted to proof systems and their associated theories and underlying complexity classes.

The book provides a number of exercises that offer insights into the presented material and facilitate understanding of the concepts and results. The list of bibliographic references contains the most representative published work in the domains of proof and computational complexity theories. As the authors suggest, the first seven chapters of the book can serve as a graduate-level text. The final chapters will be extremely valuable to researchers and doctoral students in theoretical computer science and mathematics.