December 4, 2025Open Access

On Small-depth Frege Proofs for PHP

Key Points

Exponential proof size is required for depth formulas in the Pigeon Hole Principle.
The proof must be exponential in n raised to a constant factor of 1/d based on the depth.
Random restrictions and switching lemmas are key components in the proof process.
This work highlights fundamental limitations in small-depth Frege proofs for graph theoretical principles.

Abstract

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/ (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

Demander à l'IA

Bookmark

View Full Paper