Cover -- Half-title -- Series-title -- Title -- Copyright -- CONTENTS -- PREFACE -- Chapter I: INTRODUCTION -- Chapter II: THE PREDICATE CALCULUS AND THE SYSTEM LK -- II.1. Propositional Calculus -- II.2. Predicate Calculus -- II.3. Equality Axioms -- II.4. Major Corollaries of Completeness -- II.5. The Herbrand Theorem -- II.6. Notes -- Chapter III: PEANO ARITHMETIC AND ITS SUBSYSTEMS -- III.1. Peano Arithmetic -- III.2. Parikh's Theorem -- III.3. Conservative Extensions of IΔ0 -- III.4. IΔ0 and the Linear Time Hierarchy -- III.5. Buss's… Hierarchy: The Road Not Taken -- III.6. Notes -- Chapter IV: TWO-SORTED LOGIC AND COMPLEXITY CLASSES -- IV.1. Basic Descriptive Complexity Theory -- IV.2. Two-Sorted First-Order Logic -- IV.3. Two-Sorted Complexity Classes -- IV.4. The Proof System -- IV.5. Single-Sorted Logic Interpretation -- IV.6. Notes -- Chapter V: THE THEORY V0 AND AC0 -- V.1. Definition and Basic Properties of Vi -- V.2. Two-Sorted Functions -- V.3. Parikh's Theorem for Two-Sorted Logic -- V.4. Definability in V0 -- V.5. TheWitnessing Theorem for V0 -- V.6. …: Universal Conservative Extension of V0 -- V.7. Finite Axiomatizability -- V.8. Notes -- Chapter VI: THE THEORY V1 AND POLYNOMIAL TIME -- VI.1. Induction Schemes in V1 -- VI.2. Characterizing P by V1 -- VI.3. The Replacement Axiom Scheme -- VI.4. TheWitnessing Theorem for V1 -- VI.5. Notes -- Chapter VII: PROPOSITIONAL TRANSLATIONS -- VII.1. Propositional Proof Systems -- VII.2. Translating V0 to bPK -- VII.3. Quantified Propositional Calculus -- VII.4. The Systems Gi and… -- VII.5. Propositional Translations for Vi -- VII.6. Notes -- Chapter VIII: THEORIES FOR POLYNOMIAL TIME AND BEYOND -- VIII.1. The Theory VP and Aggregate Functions -- VIII.2. The Theory VPV -- VIII.3. TV0 and the TVi Hierarchy -- VIII.4. The Theory Vi-HORN -- VIII.5. TVi and Polynomial Local Search.

VIII.6. KPT Witnessing and Replacement -- VIII.7. More on Vi and TVi -- VIII.8. RSUV Isomorphism -- VIII.9. Notes -- Chapter IX: THEORIES FOR SMALL CLASSES -- IX.1. AC0 Reductions -- IX.2. Theories for Subclasses of P -- IX.3. Theories for TC0 -- IX.4. Theories for AC0(m) and ACC -- IX.5. Theories for NC1 and the NC Hierarchy -- IX.6. Theories for NL and L -- IX.7. Open Problems -- IX.8. Notes -- Chapter X: PROOF SYSTEMS AND THE REFLECTION PRINCIPLE -- X.1. Formalizing Propositional Translations -- X.2. The Reflection Principle -- X.3. VNC1 and… -- X.4. VTC0 and Threshold Logic -- X.5. Notes -- Appendix A: COMPUTATION MODELS -- A.1. Deterministic Turing Machines -- A.2. Nondeterministic Turing Machines -- A.3. Oracle Turing Machines -- A.4. Alternating Turing Machines -- A.5. Uniform Circuit Families -- BIBLIOGRAPHY -- INDEX.