Bounded Arithmetic and Lower Bounds in Boolean Complexity

We study the question of provability of lower bounds on the complexity of explicitly given Boolean functions in weak fragments of Peano Arithmetic. To that end, we analyze what is the right fragment capturing the kind of techniques existing in Boolean complexity at present. We give both formal and informal arguments supporting the claim that a conceivable answer is V 1 1 (which, in view of RSUV-isomorphism, is equivalent to S 2 1 ), although some major results about the complexity of Boolean functions can be proved in (presumably) weaker subsystems like U 1 1 . As a by-product of this analysis, we give a more constructive version of the proof of Håstad Switching Lemma which probably is interesting in its own right. We also present, in a uniform way, theories which do not involve second order quantifiers and show that they prove the same $$\Sigma _0^{1,b}$$ -theorems as V 1 , U 1 (k ≥ 1). Another application of this technique is that the schemes of $$\Sigma _0^{1,b}$$ -replacement, $$\Sigma _0^{1,b}$$ - I N D and $$\Sigma _0^{1,b}$$ limited iterated comprehension (all of which are given by Boolean combinations of $$\Sigma _1^{1,b}$$ -formulae) together prove all $$\left( {\Sigma _1^{1,b}} \right)$$ -consequences of the full $$\Sigma _0^{1,b}$$ - I N D scheme.