Logical Foundations of Proof Complexity

  • ISBN13:


  • ISBN10:


  • Edition: 1st
  • Format: Hardcover
  • Copyright: 2010-01-25
  • Publisher: Cambridge University Press
  • Purchase Benefits
  • Free Shipping On Orders Over $35!
    Your order must be $35 or more to qualify for free economy shipping. Bulk sales, PO's, Marketplace items, eBooks and apparel do not qualify for this offer.
  • Get Rewarded for Ordering Your Textbooks! Enroll Now
List Price: $117.00 Save up to $3.51
  • Buy New
    Add to Cart Free Shipping


Supplemental Materials

What is included with this book?

  • The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.


This book treats bounded arithmetic and propositional proof complexity from the point of view of computational complexity. The first seven chapters include the necessary logical background for the material and are suitable for a graduate course. Associated with each of many complexity classes are both a two-sorted predicate calculus theory, with induction restricted to concepts in the class, and a propositional proof system. The result is a uniform treatment of many systems in the literature, including Buss's theories for the polynomial hierarchy and many disparate systems for complexity classes such as AC0, AC0(m), TC0, NC1, L, NL, NC, and P.

Author Biography

Stephen Cook is a professor at the University of Toronto. He is author or many research papers, including his famous 971 paper "The Complexity of Theorem Proving Procedures," and the 1982 recipient of the Turing Award. He was awarded a Steacie Fellowship in 1977 and a Killam Research Fellowship in 1982 and received the CRM/Fields Institute Prize in A. He is a Fellow of the royal Society of London and the royal Society of Canada and was elected to membership in the National Academy of sciences (United States) and the American Academy of Arts and Sciences. Phuong Nguyen is a postdoctoral researcher at McGill University. He received his MSc and PhD degrees from University of Toronto in 2004 and 2008, respectively. He has been awarded postdoctoral fellowships by the Eduard Cech Center for Algebra and Geometry (the Czech Republic) and by the Natural Sciences and Engineering Research Council of Canada (NSERC).

Table of Contents

Prefacep. xiii
Introductionp. 1
The Predicate Calculus and the System LKp. 9
Propositional Calculusp. 9
Gentzen's Propositional Proof System PKp. 10
Soundness and Completeness of PKp. 12
PK Proofs from Assumptionsp. 13
Propositional Compactnessp. 16
Predicate Calculusp. 17
Syntax of the Predicate Calculusp. 17
Semantics of Predicate Calculusp. 19
The First-Order Proof System LKp. 21
Free Variable Normal Formp. 23
Completeness of LK without Equalityp. 24
Equality Axiomsp. 31
Equality Axioms for LKp. 32
Revised Soundness and Completeness of LKp. 33
Major Corollaries of Completenessp. 34
The Herbrand Theoremp. 35
Notesp. 38
Peano Arithmetic and Its Subsystemsp. 39
Peano Arithmeticp. 39
Minimizationp. 44
Bounded Induction Schemep. 44
Strong Induction Schemep. 44
Parikh's Theoremp. 44
Conservative Extensions of I0p. 49
Introducing New Function and Predicate Symbolsp. 50
<$$$>: A Universal Conservative Extension of I0p. 54
Defining y = 2x and BIT(i, x) in I0p. 59
I0 and the Linear Time Hierarchyp. 65
The Polynomial and Linear Time Hierarchiesp. 65
Representability of LTH Relationsp. 66
Characterizing the LTH by I0p. 69
Buss's Si2; Hierarchy: The Road Not Takenp. 70
Notesp. 71
Two-Sorted Logic and Complexity Classesp. 73
Basic Descriptive Complexity Theoryp. 74
Two-Sorted First-Order Logicp. 76
Syntaxp. 76
Semanticsp. 78
Two-Sorted Complexity Classesp. 80
Notation for Numbers and Finite Setsp. 80
Representation Theoremsp. 81
The LTH Revisitedp. 86
The Proof System LK2p. 87
Two-Sorted Free Variable Normal Formp. 90
Single-Sorted Logic Interpretationp. 91
Notesp. 93
The Theory V0 and AC0p. 95
Definition and Basic Properties0 of Vip. 95
Two-Sorted Functionsp. 101
Parikh's Theorem for Two-Sorted Logicp. 104
Definability in V0p. 106
11-Definable Predicatesp. 115
The Witnessing Theorem for V0p. 117
Independence Follows from the Witnessing Theorem for V0p. 118
Proof of the Witnessing Theorem for V0p. 119
<$$$>: Universal Conservative Extension of V0p. 124
Alternative Proof of the Witnessing Theorem for V0p. 127
Finite Axiomatizabilityp. 129
Notesp. 130
The Theory V1 and Polynomial Timep. 133
Induction Schemes in Vip. 133
Characterizing P by V1p. 135
The "If" Direction of Theorem VI.2.2.p. 137
Application of Cobham's Theoremp. 140
The Replacement Axiom Schemep. 142
Extending V1 by Polytime Functionsp. 145
The Witnessing Theorem for V1p. 147
The Sequent System LK2-<$$$>p. 150
Proof of the Witnessing Theorem for V1p. 154
Notesp. 156
Propositional Translationsp. 159
Propositional Proof Systemsp. 160
Treelike vs Daglike Proof Systemsp. 162
The Pigeonhole Principle and Bounded Depth PKp. 163
Translating V0 to bPKp. 165
Translating B0 Formulasp. 166
<$$$> and LK2-<$$$>p. 169
Proof of the Translation Theorem for V0p. 170
Quantified Propositional Calculusp. 173
QPC Proof Systemsp. 175
The System Gp. 175
The Systems G0 and G*ip. 179
Extended Frege Systems and Witnessing in G*1p. 186
Propositional Translations for Vip. 191
Translating V0 to Bounded Depth G*0p. 195
Notesp. 198
Theories for Polynomial Time and Beyondp. 201
The Theory VP and Aggregate Functionsp. 201
The Theory <$$$>p. 207
The Theory VPVp. 210
Comparing VPV and V1p. 213
VPV Is Conservative over VPp. 214
TV0 and the TVi Hierarchyp. 217
TV0 ⊆ VPVp. 220
Bit Recursionp. 222
The Theory V1-HORNp. 223
TV1 and Polynomial Local Searchp. 228
KPT Witnessing and Replacementp. 237
Applying KPT Witnessingp. 239
More on Vi and TVip. 243
Finite Axiomatizabilityp. 243
Definability in the V? Hierarchyp. 245
Collapse of V? vs Collapse of PHp. 253
RSUV Isomorphismp. 256
The Theories Si2 and Ti2p. 256
RSUV Isomorphismp. 258
The # Translationp. 260
The b Translationp. 262
The RSUV Isomorphism between Si2 and Vip. 263
Notesp. 266
Theories for Small Classesp. 267
AC0 Reductionsp. 269
Theories for Subclasses of Pp. 272
The Theories VCp. 273
The Theory <$$$>p. 274
The Theory <$$$>p. 278
Obtaining Theories for the Classes of Interestp. 280
Theories for TC0p. 281
The Class TC0p. 282
The Theories VTC0, <$$$>, and <$$$>p. 283
Number Recursion and Number Summationp. 287
The Theory VTC0Vp. 289
Proving the Pigeonhole Principle in VTC0p. 291
Denning String Multiplication in VTC0p. 293
Proving Finite Szpilrajn's Theorem in VTC0p. 298
Proving Bondy's Theoremp. 299
Theories for AC0 (m) and ACCp. 303
The Classes AC0 (m) and ACCp. 303
The Theories V0(2), <$$$>, and <$$$>p. 304
The "onto" PHP and Parity Principlep. 306
The Theory VAC0 (2)Vp. 308
The Jordan Curve Theorem and Related Principlesp. 309
The Theories for AC0 (m) and ACCp. 313
The Modulo m Counting Principlesp. 316
The Theory VAC0 (6)Vp. 318
Theories for NC1 and the NC Hierarchyp. 319
Definitions of the Classesp. 320
BSVP and NC1p. 321
The Theories VNC1, <$$$>, and <$$$>p. 323
VTC0 ⊆ VNC1p. 326
The Theory VNC1 Vp. 333
Theories for the NC Hierarchyp. 335
Theories for NL and Lp. 339
The Theories VNL, <$$$>, and <$$$>p. 339
The Theory V1-KROMp. 343
The Theories VL, <$$$>, and <$$$>p. 351
The Theory VLVp. 356
Open Problemsp. 358
Proving Cayley-Hamilton in VNC2p. 358
VSL and VSL <$$$> VLp. 358
Denning [X/Y] in VTC0p. 360
Proving PHP and Countm′ in V0 (m)p. 360
Notesp. 360
Proof Systems and the Reflection Principlep. 363
Formalizing Propositional Translationsp. 364
Verifying Proofs in TC0p. 364
Computing Propositional Translations in TC0p. 373
The Propositional Translation Theorem for TVip. 377
The Reflection Principlep. 382
Truth Definitionsp. 383
Truth Definitions vs Propositional Translationsp. 387
RFN and Consistency for Subsystems of Gp. 396
Axiomatizations Using RFNp. 403
Proving -Simulations Using RFNp. 407
The Witnessing Problems for Gp. 408
VNC1 and G*0p. 410
Propositional Translation for VNC1p. 410
The Boolean Sentence Value Problemp. 414
Reflection Principle for PKp. 421
VTC0 and Threshold Logicp. 428
The Sequent Calculus PTKp. 428
Reflection Principles for Bounded Depth PTKp. 433
Propositional Translation for VTC0p. 434
Bounded Depth GTC0p. 441
Notesp. 442
Computation Modelsp. 445
Deterministic Turing Machinesp. 445
L, P, PSPACE, and EXPp. 447
Nondeterministic Turing Machinesp. 449
Oracle Turing Machinesp. 451
Alternating Turing Machinesp. 452
Uniform Circuit Familiesp. 453
Bibliographyp. 457
Indexp. 465
Table of Contents provided by Ingram. All Rights Reserved.

Rewards Program

Write a Review