Tradeoffs for small-depth Frege proofs

TL;DR

This paper establishes new tradeoffs between the size of individual lines and the number of lines in small-depth Frege proofs, providing stronger lower bounds than previous results for certain proof parameters.

Contribution

It introduces the first tradeoff bounds between line size and number of lines in small-depth Frege proofs, connecting circuit complexity techniques to proof complexity.

Findings

Proves exponential lower bounds on the number of lines for depth-d Frege proofs of Tseitin on grids.

Shows these bounds are stronger than previous overall proof size bounds in certain regimes.

Demonstrates that circuit correlation bounds can be applied to proof complexity tradeoffs.

Abstract

We study the complexity of small-depth Frege proofs and give the first tradeoffs between the size of each line and the number of lines. Existing lower bounds apply to the overall proof size -- the sum of sizes of all lines -- and do not distinguish between these notions of complexity. For depth-$d$ Frege proofs of the Tseitin principle on the $n \times n$ grid where each line is a size-$s$ formula, we prove that $\exp(n/2^{\Omega(d\sqrt{\log s})})$ many lines are necessary. This yields new lower bounds on line complexity that are not implied by H{\aa}stad's recent $\exp(n^{\Omega(1/d)})$ lower bound on the overall proof size. For $s = \mathrm{poly}(n)$, for example, our lower bound remains $\exp(n^{1-o(1)})$ for all $d = o(\sqrt{\log n})$, whereas H{\aa}stad's lower bound is $\exp(n^{o(1)})$ once $d = \omega_n(1)$. Our main conceptual contribution is the simple observation that techniques for establishing correlation bounds in circuit complexity can be leveraged to establish such tradeoffs in proof complexity.