# Logical Foundations of Proof Complexity

A treatise on bounded arithmetic and propositional proof complexity by the leader in the field.See more details below

## Overview

A treatise on bounded arithmetic and propositional proof complexity by the leader in the field.

## 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)

## Related Subjects

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