Abstract
A map g : {0, 1}n → {0, 1}m (m > n) is a hard proof complexity generator for a proof system P iff for every string b ∈ {0, 1}m \ Rng(g), formula τb(g) naturally expressing b ∉ Rng(g) requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is Nisan-Wigderson generator. Razborov [37] conjectured that if A is a suitable matrix and f is a NP ∩ CoNP function hard-on-average for P/poly, then NWf,A is a hard proof complexity generator for Extended Frege. In this paper, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP ∩ CoNP function f that is exponentially hard for depth two AC0 circuits, NWf,A is a hard proof complexity generator for AC0-Frege in a natural setting. As direct applications of this theorem, we show that:
1. For any f with the specified properties, τb(NWf,A) (for a natural formalization) based on a random b and a random matrix A with probability 1 − o(1) is a tautology and requires superpolynomial (or even exponential) AC0-Frege proofs.
2. Certain formalizations of the principle fn∉(NP∩CoNP)/poly requires superpolynomial AC0-Frege proofs.
These applications relate to two questions that were asked by Krajíček [21].