Observational analysis reveals exponential proof size for the Pigeon Hole Principle in graphs, indicating significant constraints on depth formulas.
We study Frege proofs for the one-to-one graph Pigeon Hole Principle defined on the n× 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 , , and . 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. 42 pages. This is the TheoretiCS journal version
No takes yet. Share an insight, caveat, or question.
Johan Håstad (2025) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: