Logical Foundations of Proof Complexity

by Stephen Cook, Phuong Nguyen

Overview

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.

Product Details

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

About 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.

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Δ₀ 49

III.3.1 Introducing New Function and Predicate Symbols 50

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

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

III.4 IΔ₀ 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Δ₀ 69

III.5 Buss's Sⁱ₂; 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 LK² 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 V⁰ and AC⁰ 95

V.1 Definition and Basic Properties0 of Vⁱ 95

V.2 Two-Sorted Functions 101

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

V.4 Definability in V⁰ 106

V.4.1 Δ ¹₁-Definable Predicates 115

V.5 The Witnessing Theorem for V⁰ 117

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

V.5.2 Proof of the Witnessing Theorem for V⁰ 119

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

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

V.7 Finite Axiomatizability 129

V.8 Notes 130

Chapter VI The Theory V¹ and Polynomial Time 133

VI.l Induction Schemes in Vⁱ 133

VI.2 Characterizing P by V¹ 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 V¹ by Polytime Functions 145

VI.4 The Witnessing Theorem for V¹ 147

VI.4.1 The Sequent System LK²-<$$$> 150

VI.4.2 Proof of the Witnessing Theorem for V¹ 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 V⁰ to bPK 165

VII.2.1 Translating Σ^B₀ Formulas 166

VII.2.2 <$$$> and LK²-<$$$> 169

VII.2.3 Proof of the Translation Theorem for V⁰ 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 G₀ and G^*_i 179

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

VII.5 Propositional Translations for Vⁱ 191

VII.5.1 Translating V⁰ to Bounded Depth G^*₀ 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 V¹ 213

VIII.2.2 VPV Is Conservative over VP 214

VIII.3 TV⁰ and the TVⁱ Hierarchy 217

VIII.3.1 TV⁰ ⊆ VPV 220

VIII.3.2 Bit Recursion 222

VIII.4 The Theory V¹-HORN 223

VIII.5 TV¹ and Polynomial Local Search 228

VIII.6 KPT Witnessing and Replacement 237

VIII6.1 Applying KPT Witnessing 239

VIII.7 More on Vⁱ and TVⁱ 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 Sⁱ₂ and Tⁱ₂ 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 Sⁱ₂ and Vⁱ 263

VIII.9 Notes 266

Chapter IX Theories for Small Classes 267

IX.1 AC⁰ 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 TC⁰ 281

IX.3.1 The Class TC⁰ 282

IX.3.2 The Theories VTC⁰, <$$$>, and <$$$> 283

IX.3.3 Number Recursion and Number Summation 287

IX.3.4 The Theory VTC⁰V 289

IX.3.5 Proving the Pigeonhole Principle in VTC⁰ 291

IX.3.6 Denning String Multiplication in VTC⁰ 293

IX.3.7 Proving Finite Szpilrajn's Theorem in VTC⁰ 298

IX.3.8 Proving Bondy's Theorem 299

IX.4 Theories for AC⁰ (m) and ACC 303

IX.4.1 The Classes AC⁰ (m) and ACC 303

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

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

IX.4.4 The Theory VAC⁰ (2)V 308

IX.4.5 The Jordan Curve Theorem and Related Principles 309

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

IX.4.7 The Modulo m Counting Principles 316

IX.4.8 The Theory VAC⁰ (6)V 318

IX.5 Theories for NC¹ and the NC Hierarchy 319

IX.5.1 Definitions of the Classes 320

IX.5.2 BSVP and NC¹ 321

IX.5.3 The Theories VNC¹, <$$$>, and <$$$> 323

IX.5.4 VTC⁰ ⊆ VNC¹ 326

IX.5.5 The Theory VNC¹ 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 V¹-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 VNC² 358

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

IX.7.3 Denning [X/Y] in VTC⁰ 360

IX.7.4 Proving PHP and Count_m′ in V⁰ (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 TC⁰ 364

X.1.2 Computing Propositional Translations in TC⁰ 373

X.l.3 The Propositional Translation Theorem for TVⁱ 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 VNC¹ and G^*₀ 410

X.3.1 Propositional Translation for VNC¹ 410

X.3.2 The Boolean Sentence Value Problem 414

X.3.3 Reflection Principle for PK 421

X.4 VTC⁰ 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 VTC⁰ 434

X.4.4 Bounded Depth GTC⁰ 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

Editorial Reviews

"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

From the Publisher