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. We ask for short propositional proofs of circuit lower bounds expressed succinctly by propositional formulas of size n(O)((1)) or at least much smaller than the 2(O(n)) size of the common "truth table" formula. We discuss two such expressions: one via feasible functions witnessing errors of circuits, and one via the anticheckers of Lipton and Young 1994. Our APC(1) formalizations yield conditional upper bounds for the succinct formulas obtained by witnessing: we get short Extended Frege proofs from general circuit lower bounds expressed by the common "truth-table" formulas. We also show how to construct in quasipolynomial time propositional proofs of quasipolynomial size tautologies expressing AC(0)[p] quasipolynomial size lower bounds; these proofs are in Jefabek's system WF. (C) 2019 Elsevier B.V. All rights reserved.