Logical Foundations of Proof Complexity

Hardcover (Print)
Used and New from Other Sellers
Used and New from Other Sellers
from $95.39
Usually ships in 1-2 business days
Other sellers (Hardcover)
  • All (9) from $95.39   
  • New (5) from $95.39   
  • Used (4) from $99.14   


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.

Read More Show Less

Editorial Reviews

From the Publisher
"This authoritative volume on computational complexity of logical systems provides a sound background in logic for computer science and mathematics students. The book provides a number of exercises that offer insights into the presented material and facilitate the 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."
L. State, reviews.com

"This most erudite of books will stand the test of time. I will revisit it often."
George Hacken, Computing Reviews

"... very great detail and with care... The presentation of the book is most thorough and the treatment rigorous, providing the reader with the right amount of intuition and detail to follow even complicated constructions. The new book by Cook and Nguyen will become another classic for the field of bounded arithmetic and its relations to computational complexity and propositional proof complexity. It will serve as a rich source of reference for the expert and as a thorough guide to the student interested in learning about this beautiful field."
Olaf Beyersdorff, Mathematical Reviews

Read More Show Less

Product Details

  • ISBN-13: 9780521517294
  • Publisher: Cambridge University Press
  • Publication date: 1/25/2010
  • Series: Perspectives in Logic Series
  • Pages: 496
  • Product dimensions: 6.30 (w) x 9.30 (h) x 1.30 (d)

Meet the Author

Stephen Cook is a professor at the University of Toronto. He is author of many research papers, including his famous 1971 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 1999. 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 (Nguyễn Thế Phương) received his MSc and PhD degrees from University of Toronto in 2004 and 2008 respectively. He has been awarded postdoctoral fellowships by the Eduard Čech Center for Algebra and Geometry (the Czech Republic) for 2008–9, and by the Natural Sciences and Engineering Research Council of Canada (NSERC), effective September 2009.

Read More Show Less

Table of Contents

Preface xiii

Chapter I Introduction 1

Chapter II The Predicate Calculus and the System LK 9

II.1 Propositional Calculus 9

II.1.1 Gentzen's Propositional Proof System PK 10

II.1.2 Soundness and Completeness of PK 12

II.1.3 PK Proofs from Assumptions 13

II.1.4 Propositional Compactness 16

II.2 Predicate Calculus 17

II.2.1 Syntax of the Predicate Calculus 17

II.2.2 Semantics of Predicate Calculus 19

II.2.3 The First-Order Proof System LK 21

II.2.4 Free Variable Normal Form 23

II.2.5 Completeness of LK without Equality 24

II.3 Equality Axioms 31

II.3.1 Equality Axioms for LK 32

II.3.2 Revised Soundness and Completeness of LK 33

II.4 Major Corollaries of Completeness 34

II.5 The Herbrand Theorem 35

II.6 Notes 38

Chapter III Peano Arithmetic and Its Subsystems 39

III.1 Peano Arithmetic 39

III.l.1 Minimization 44

III.1.2 Bounded Induction Scheme 44

III.1.3 Strong Induction Scheme 44

III.2 Parikh's Theorem 44

III.3 Conservative Extensions of IΔ0 49

III.3.1 Introducing New Function and Predicate Symbols 50

III.3.2 <$$$>: A Universal Conservative Extension of IΔ0 54

III.3.3 Defining y = 2x and BIT(i, x) in IΔ0 59

III.4 IΔ0 and the Linear Time Hierarchy 65

III.4.1 The Polynomial and Linear Time Hierarchies 65

III.4.2 Representability of LTH Relations 66

III.4.3 Characterizing the LTH by IΔ0 69

III.5 Buss's Si2; Hierarchy: The Road Not Taken 70

III.6 Notes 71

Chapter IV Two-Sorted Logic and Complexity Classes 73

IV.1 Basic Descriptive Complexity Theory 74

IV.2 Two-Sorted First-Order Logic 76

IV.2.1 Syntax 76

IV.2.2 Semantics 78

IV.3 Two-Sorted Complexity Classes 80

IV.3.1 Notation for Numbers and Finite Sets 80

IV.3.2 Representation Theorems 81

IV.3.3 The LTH Revisited 86

IV.4 The Proof System LK2 87

IV.4.1 Two-Sorted Free Variable Normal Form 90

IV.5 Single-Sorted Logic Interpretation 91

IV.6 Notes 93

Chapter V The Theory V0 and AC0 95

V.1 Definition and Basic Properties0 of Vi 95

V.2 Two-Sorted Functions 101

V.3 Parikh's Theorem for Two-Sorted Logic 104

V.4 Definability in V0 106

V.4.1 Δ 11-Definable Predicates 115

V.5 The Witnessing Theorem for V0 117

V.5.1 Independence Follows from the Witnessing Theorem for V0 118

V.5.2 Proof of the Witnessing Theorem for V0 119

V.6 <$$$>: Universal Conservative Extension of V0 124

V.6.1 Alternative Proof of the Witnessing Theorem for V0 127

V.7 Finite Axiomatizability 129

V.8 Notes 130

Chapter VI The Theory V1 and Polynomial Time 133

VI.l Induction Schemes in Vi 133

VI.2 Characterizing P by V1 135

VI.2.1 The "If" Direction of Theorem VI.2.2. 137

VI.2.2 Application of Cobham's Theorem 140

VI.3 The Replacement Axiom Scheme 142

VI.3.1 Extending V1 by Polytime Functions 145

VI.4 The Witnessing Theorem for V1 147

VI.4.1 The Sequent System LK2-<$$$> 150

VI.4.2 Proof of the Witnessing Theorem for V1 154

VI.5 Notes 156

Chapter VII Propositional Translations 159

VII.1 Propositional Proof Systems 160

VII.1.1 Treelike vs Daglike Proof Systems 162

VII.1.2 The Pigeonhole Principle and Bounded Depth PK 163

VII.2 Translating V0 to bPK 165

VII.2.1 Translating ΣB0 Formulas 166

VII.2.2 <$$$> and LK2-<$$$> 169

VII.2.3 Proof of the Translation Theorem for V0 170

VII.3 Quantified Propositional Calculus 173

VII.3.1 QPC Proof Systems 175

VII.3.2 The System G 175

VIL.4 The Systems G0 and G*i 179

VII.4.1 Extended Frege Systems and Witnessing in G*1 186

VII.5 Propositional Translations for Vi 191

VII.5.1 Translating V0 to Bounded Depth G*0 195

VII.6 Notes 198

Chapter VIII Theories for Polynomial Time and Beyond 201

VIII.l The Theory VP and Aggregate Functions 201

VIII.1.1 The Theory <$$$> 207

VIII.2 The Theory VPV 210

VIII.2.1 Comparing VPV and V1 213

VIII.2.2 VPV Is Conservative over VP 214

VIII.3 TV0 and the TVi Hierarchy 217

VIII.3.1 TV0 ⊆ VPV 220

VIII.3.2 Bit Recursion 222

VIII.4 The Theory V1-HORN 223

VIII.5 TV1 and Polynomial Local Search 228

VIII.6 KPT Witnessing and Replacement 237

VIII6.1 Applying KPT Witnessing 239

VIII.7 More on Vi and TVi 243

VIII.7.1 Finite Axiomatizability 243

VIII.7.2 Definability in the V? Hierarchy 245

VIII.7.3 Collapse of V? vs Collapse of PH 253

VIII.8 RSUV Isomorphism 256

VIII.8.1 The Theories Si2 and Ti2 256

VIII.8.2 RSUV Isomorphism 258

VIII.8.3 The # Translation 260

VIII.8.4 The b Translation 262

VIII.8.5 The RSUV Isomorphism between Si2 and Vi 263

VIII.9 Notes 266

Chapter IX Theories for Small Classes 267

IX.1 AC0 Reductions 269

IX.2 Theories for Subclasses of P 272

IX.2.1 The Theories VC 273

IX.2.2 The Theory <$$$> 274

IX.2.3 The Theory <$$$> 278

IX.2.4 Obtaining Theories for the Classes of Interest 280

IX.3 Theories for TC0 281

IX.3.1 The Class TC0 282

IX.3.2 The Theories VTC0, <$$$>, and <$$$> 283

IX.3.3 Number Recursion and Number Summation 287

IX.3.4 The Theory VTC0V 289

IX.3.5 Proving the Pigeonhole Principle in VTC0 291

IX.3.6 Denning String Multiplication in VTC0 293

IX.3.7 Proving Finite Szpilrajn's Theorem in VTC0 298

IX.3.8 Proving Bondy's Theorem 299

IX.4 Theories for AC0 (m) and ACC 303

IX.4.1 The Classes AC0 (m) and ACC 303

IX.4.2 The Theories V0(2), <$$$>, and <$$$> 304

IX.4.3 The "onto" PHP and Parity Principle 306

IX.4.4 The Theory VAC0 (2)V 308

IX.4.5 The Jordan Curve Theorem and Related Principles 309

IX.4.6 The Theories for AC0 (m) and ACC 313

IX.4.7 The Modulo m Counting Principles 316

IX.4.8 The Theory VAC0 (6)V 318

IX.5 Theories for NC1 and the NC Hierarchy 319

IX.5.1 Definitions of the Classes 320

IX.5.2 BSVP and NC1 321

IX.5.3 The Theories VNC1, <$$$>, and <$$$> 323

IX.5.4 VTC0 ⊆ VNC1 326

IX.5.5 The Theory VNC1 V 333

IX.5.6 Theories for the NC Hierarchy 335

IX.6 Theories for NL and L 339

IX.6.1 The Theories VNL, <$$$>, and <$$$> 339

IX.6.2 The Theory V1-KROM 343

IX.6.3 The Theories VL, <$$$>, and <$$$> 351

IC.6.4 The Theory VLV 356

IX.7 Open Problems 358

IX.7.1 Proving Cayley-Hamilton in VNC2 358

IX.7.2 VSL and VSL <$$$> VL 358

IX.7.3 Denning [X/Y] in VTC0 360

IX.7.4 Proving PHP and Countm′ in V0 (m) 360

IX.8 Notes 360

Chapter X Proof Systems and the Reflection Principle 363

X.l Formalizing Propositional Translations 364

X.l.l Verifying Proofs in TC0 364

X.1.2 Computing Propositional Translations in TC0 373

X.l.3 The Propositional Translation Theorem for TVi 377

X.2 The Reflection Principle 382

X.2.1 Truth Definitions 383

X.2.2 Truth Definitions vs Propositional Translations 387

X.2.3 RFN and Consistency for Subsystems of G 396

X.2.4 Axiomatizations Using RFN 403

X.2.5 Proving -Simulations Using RFN 407

X.2.6 The Witnessing Problems for G 408

X.3 VNC1 and G*0 410

X.3.1 Propositional Translation for VNC1 410

X.3.2 The Boolean Sentence Value Problem 414

X.3.3 Reflection Principle for PK 421

X.4 VTC0 and Threshold Logic 428

X.4.1 The Sequent Calculus PTK 428

X.4.2 Reflection Principles for Bounded Depth PTK 433

X.4.3 Propositional Translation for VTC0 434

X.4.4 Bounded Depth GTC0 441

X.5 Notes 442

Appendix A Computation Models 445

A.l Deterministic Turing Machines 445

A.11 L, P, PSPACE, and EXP 447

A.2 Nondeterministic Turing Machines 449

A.3 Oracle Turing Machines 451

A.4 Alternating Turing Machines 452

A.5 Uniform Circuit Families 453

Bibliography 457

Index 465

Read More Show Less

Customer Reviews

Be the first to write a review
( 0 )
Rating Distribution

5 Star


4 Star


3 Star


2 Star


1 Star


Your Rating:

Your Name: Create a Pen Name or

Barnes & Noble.com Review Rules

Our reader reviews allow you to share your comments on titles you liked, or didn't, with others. By submitting an online review, you are representing to Barnes & Noble.com that all information contained in your review is original and accurate in all respects, and that the submission of such content by you and the posting of such content by Barnes & Noble.com does not and will not violate the rights of any third party. Please follow the rules below to help ensure that your review can be posted.

Reviews by Our Customers Under the Age of 13

We highly value and respect everyone's opinion concerning the titles we offer. However, we cannot allow persons under the age of 13 to have accounts at BN.com or to post customer reviews. Please see our Terms of Use for more details.

What to exclude from your review:

Please do not write about reviews, commentary, or information posted on the product page. If you see any errors in the information on the product page, please send us an email.

Reviews should not contain any of the following:

  • - HTML tags, profanity, obscenities, vulgarities, or comments that defame anyone
  • - Time-sensitive information such as tour dates, signings, lectures, etc.
  • - Single-word reviews. Other people will read your review to discover why you liked or didn't like the title. Be descriptive.
  • - Comments focusing on the author or that may ruin the ending for others
  • - Phone numbers, addresses, URLs
  • - Pricing and availability information or alternative ordering information
  • - Advertisements or commercial solicitation


  • - By submitting a review, you grant to Barnes & Noble.com and its sublicensees the royalty-free, perpetual, irrevocable right and license to use the review in accordance with the Barnes & Noble.com Terms of Use.
  • - Barnes & Noble.com reserves the right not to post any review -- particularly those that do not follow the terms and conditions of these Rules. Barnes & Noble.com also reserves the right to remove any review at any time without notice.
  • - See Terms of Use for other conditions and disclaimers.
Search for Products You'd Like to Recommend

Recommend other products that relate to your review. Just search for them below and share!

Create a Pen Name

Your Pen Name is your unique identity on BN.com. It will appear on the reviews you write and other website activities. Your Pen Name cannot be edited, changed or deleted once submitted.

Your Pen Name can be any combination of alphanumeric characters (plus - and _), and must be at least two characters long.

Continue Anonymously

    If you find inappropriate content, please report it to Barnes & Noble
    Why is this product inappropriate?
    Comments (optional)