Provability of the Circuit Size Hierarchy and Its Consequences

The Circuit Size Hierarchy (CSH^a) states that if a > b ≥ 1 then the set of functions on n variables computed by Boolean circuits of size n^a is strictly larger than the set of functions computed by circuits of size n^b. This result, which is a cornerstone of circuit complexity theory, follows from the non-constructive proof of the existence of functions of large circuit complexity obtained by Shannon in 1949. Are there more “constructive” proofs of the Circuit Size Hierarchy? Can we quantify this? Motivated by these questions, we investigate the provability of CSH^a in theories of bounded arithmetic. Among other contributions, we establish the following results: (i) Given any a > b > 1, CSH^a is provable in Buss’s theory T². (ii) In contrast, if there are constants a > b > 1 such that CSH^a is provable in the theory T¹, then there is a constant ε > 0 such that P^NP requires non-uniform circuits of size at least n^1+ε. In other words, an improved upper bound on the proof complexity of CSH^a would lead to new lower bounds in complexity theory. We complement these results with a proof of the Formula Size Hierarchy (FSH^a) in PV1 with parameters a > 2 and b = 3/2. This is in contrast with typical formalizations of complexity lower bounds in bounded arithmetic, which require APC1 or stronger theories and are not known to hold even in T¹