Feasibly constructive proofs of succinct weak circuit lower bounds

摘要

We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length n. In 1995 Razborov showed that many can be proved in PV1, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small n of doubly logarithmic order. It is open whether PV1 proves known lower bounds in succinct formalizations for n of logarithmic order. We give such proofs in APC(1), an extension of PV1 formalizing probabilistic polynomial time reasoning: for parity and AC(0), for mod q and AC(0) [p] (only for n slightly smaller than logarithmic), and for k-clique and monotone circuits. We also formalize Razborov and Rudich's natural proof barrier.