In this thesis we investigate the power of weak fragments of arithmetic. We do this from a model theoretic and also from a proof complexity perspective. From a model theoretic point of view it seems reasonable that a small initial segment of any model of bounded arithmetic is a model of a stronger theory. We exemplify this by showing that any polylogarithmic cut of a model of V^0 is actually a model of VNC. Exploiting a well-known connection between frag- ments of bounded arithmetic and provability in various proof systems, we show a separation result between Resolution and the TC^0-Frege proof system on random 3CNF within a certain clause-to-variable ratio. Combining both results we can also conclude a weaker separation result for Resolution and bounded depth Frege systems.
1 Preliminaries 6
1.1 Proof Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.1.1 Some Important Proof Systems and Their Interrelation . . 7
1.2 Bounded Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.3 The Theory V0 and its Extensions . . . . . . . . . . . . . . . . . 15
1.3.1 The Theory VTC0 . . . . . . . . . . . . . . . . . . . . . . 18
1.3.2 The Theories VNCk and VNC . . . . . . . . . . . . . . . 20
1.3.3 Relation between Arithmetic Theories and Proof Systems . 22
2 Refutations of Random 3CNF in TC0-Frege 26
2.0.4 Step I. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.0.5 Step II. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3 Cuts of Models of V0 32
3.1 Polylogarithmic Cuts and VNC1 . . . . . . . . . . . . . . . . . . 33
3.2 Polylogarithmic Cuts and VNC . . . . . . . . . . . . . . . . . . . 34
4 Computations in VTC0 37
4.1 DH and extensions of VTC0 . . . . . . . . . . . . . . . . . . . . . 38
4.1.1 Proving EXP_{G;P} . . . . . . . . . . . . . . . . . . . . . . . . 41
5 Conclusion 45
A Short Refutations for Random 3CNF 1
A.0.2 Background in proof complexity . . . . . . . . . . . . . . . 1
A.0.3 Our result . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
A.0.4 Relations to previous works . . . . . . . . . . . . . . . . . 5
A.0.5 The structure of the argument . . . . . . . . . . . . . . . . 6
A.0.6 Overview of the Proof . . . . . . . . . . . . . . . . . . . . 8
A.0.7 Organization of the paper . . . . . . . . . . . . . . . . . . 12
A.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
A.1.1 Miscellaneous linear algebra notations . . . . . . . . . . . 13
A.1.2 Propositional proofs and TC0-Frege systems . . . . . . . . 13
A.2 Theories of Bounded Arithmetic . . . . . . . . . . . . . . . . . . . 16
A.2.1 The theory V0 . . . . . . . . . . . . . . . . . . . . . . . . 17
A.2.2 The theory VTC0 . . . . . . . . . . . . . . . . . . . . . . 24
A.3 Feige-Kim-Ofek Witnesses and the Main Formula . . . . . . . . . 36
A.4 Proof of the Main Formula . . . . . . . . . . . . . . . . . . . . . . 39
A.4.1 Formulas satisfied as 3XOR . . . . . . . . . . . . . . . . . 44
A.4.2 Bounding the number of NAE satisfying assignments . . . 46
A.5 The Spectral Bound . . . . . . . . . . . . . . . . . . . . . . . . . 48
A.5.1 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
A.5.2 Rational approximations of Reals, vectors and matrices . . 49
A.5.3 The predicate EigValBound . . . . . . . . . . . . . . . . 50
A.5.4 Certifying the spectral inequality . . . . . . . . . . . . . . 53
A.6 Wrapping-up the Proof: TC0-Frege Refutations of Random 3CNF 57
A.6.1 Converting the main formula into a Sigma^B_0 formula . . . . . 57
A.6.2 Propositional proofs . . . . . . . . . . . . . . . . . . . . . 58
A.7 Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
B Polylogarithmic Cuts of Models of V^0 62
B.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
B.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
B.2.1 Elements of Proof Complexity . . . . . . . . . . . . . . . . 64
B.2.2 The theory V0 . . . . . . . . . . . . . . . . . . . . . . . . 65
B.2.3 Extensions of V0 . . . . . . . . . . . . . . . . . . . . . . . 68
B.2.4 Relation between Arithmetic Theories and Proof Systems . 68
B.3 Polylogarithmic Cuts of Models of V^0 are Models of VNC^1. . . . 70
B.4 Implications for Proof Complexity . . . . . . . . . . . . . . . . . . 75
B.5 Conclusion and Discussion . . . . . . . . . . . . . . . . . . . . . . 75
B.6 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . 76
C Necessary Background 77
C.1 Logical Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . 77
C.1.1 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . 78
C.1.2 First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . 82
C.2 Complexity Theory . . . . . . . . . . . . . . . . . . . . . . . . . . 85
C.2.1 Circuit Complexity . . . . . . . . . . . . . . . . . . . . . . 89