On Small-depth Frege Proofs for PHP
Johan Håstad
TL;DR
This work establishes exponential lower bounds for small-depth Frege proofs refuting the functional and onto Pigeon Hole Principle on an odd grid, showing size exp(Ω(n^{1/(2d-1)}(log n)^{O(1)})) and, with line-size limits, line counts exp(Ω(n/(log M)^{O(d)})). The core method introduces a novel restriction design that preserves the PHP structure on the grid and a multi-switching lemma to handle many small-depth formulas simultaneously, together with t-evaluations and locally consistent partial matchings to control proof behavior under restrictions. By combining these techniques, the authors extend the switch-based lower-bound program to the grid PHP and derive both total-size and line-count lower bounds, providing new insights into the depth-size trade-offs for Frege proofs in grid-like combinatorial tautologies. The results deepen our understanding of proof complexity for PHP-like principles and offer versatile tools (restriction spaces, multi-switching, and canonical decision trees) potentially applicable to other small-depth proof and circuit settings.
Abstract
We study Frege proofs for the one-to-one graph Pigeon Hole Principle defined on the $n\times n$ grid where $n$ is odd. We are interested in the case where each formula in the proof is a depth $d$ formula in the basis given by $\land$, $\lor$, and $\neg$. We prove that in this situation the proof needs to be of size exponential in $n^{Ω(1/d)}$. If we restrict the size of each line in the proof to be of size $M$ then the number of lines needed is exponential in $n/(\log M)^{O(d)}$. The main technical component of the proofs is to design a new family of random restrictions and to prove the appropriate switching lemmas.