A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic

Abstract

The aim of this work is to formalize the circuit-size lower bound showed by Kannan in 1982 in a weak theory for feasible computations. In particular, we will work with theories of bounded arithmetic, which are subtheories of Peano Arithmetic that weaken its induction axiom scheme by restricting it to formulas in which the quantifiers are bounded. Kannan’s circuit lower bound states that for every fixed polynomial size of circuits, there is a language in the second level of the polynomial hierarchy that cannot be decided by circuits of that size. We note that the essential ingredient in this proof is a key use of the weak pigeonhole principle, which is available in bounded arithmetic. Instrumental in the proof of Kannan’s Theorem is the celebrated Karp-Lipton’s Theorem, stating that if the satisfiability problem for propositional formulas can be decided by polynomial-size circuits then the polynomial hierarchy collapses to its second level, which we also formalize in the same theory