Towards P≠NP from Extended Frege Lower Bounds

We give a new approach to the fundamental question of whether proof complexity lower bounds for concrete propositional proof systems imply super-polynomial Boolean circuit lower bounds. We observe that any general implication from proof complexity lower bounds for a propositional proof system to super-polynomial Boolean circuit lower bounds implies unconditionally that NEXP does not have Boolean circuits of polynomial size. We explore connections that are possible to establish without settling this long-standing and famously hard open question. For any poly-time computable function f, we define the witnessing formulas w(n)(k)(f), which are propositional formulas stating that for any circuit C of size n(k) on n variables and for any formula phi of size n, either C computes a satisfying assignment to q5 or f verifiably refutes that C computes SAT on instances of length n. We show that if the witnessing formulas are tautologies, then any super-polynomial lower bound for Extended Frege augmented with w(n)(k)(f) axioms implies that SAT requires super-polynomial size Boolean circuits. We also give an unconditional equivalence between circuit lower bounds for the Discrete Logarithm problem and proof complexity lower bounds (for propositional formulas efficiently encoding the statement that the Discrete Logarithm problem is computable by small circuits) for a concretely defined strong (non-uniform) propositional proof system. We give consequences of our connections for the meta-mathematics of several major questions in computational complexity, including whether one-way functions can be based on the worst-case hardness of NP, whether there is a dichotomy between one-way functions and worst-case learning with membership queries over the uniform distribution, and whether there are feasibly constructible anti-checkers for Satisfiability. We show that for each of these questions, provability of a positive answer in essentially any standard mathematical theory would imply new connections between propositional proof complexity and circuit complexity. Our results rely on a new notion of "self-provability" of upper bounds, which might be independently interesting, and involve a novel application of random self-reducibility to proof complexity.