Tradeoffs for small-depth Frege proofs

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 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$\mathbf{H}\mathop{\mathbf{a}}\!\!\!\!^{\circ}\mathbf{stad}$'s recent$\exp(n^{\Omega(1/d)})$lower bound on the overall proof size. For$s$= poly$(n)$, for example, our lower bound remains$\exp(n^{1-o(1)})$for all$d=o(\sqrt{\log n})$, whereas$\mathbf{H}\mathop{\mathbf{a}}\!\!\!\!^{\circ}\mathbf{stad}$'s lower bound is$\exp(n^{o(1)})$once$d\ = \omega_{n}(1)$. Our main conceptual contribution is the simple obser-vation that techniques for establishing correlation bounds in circuit complexity can be leveraged to establish such tradeoffs in proof complexity.