__
TR23-042 | 3rd April 2023 14:46
__

#### On small-depth Frege proofs for PHP

**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^{\Omega (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.