Exponential lower bounds for the pigeonhole principle (Q687506)

The paper deals with complexity of Frege proofs for the (propositional) pigeonhole principle (\(\text{PHP}_ n\) for all natural \(n\)). It shows an exponential lower bound on the size of proofs with bounded depth (of logical connectives in formulas). Thus the previously known superpolynomial lower bound by Ajtai has been improved. As a corollary, the authors obtained an \(\Omega(\log\log n)\) lower bound on depth for polynomial-size Frege proofs of \(\text{PHP}_ n\). It is close to the precise complexity since Buss has constructed polynomial- size, logarithmic-depth proofs for \(\text{PHP}_ n\). The proof goes by induction on the depth -- using a certain approximation of the depth \(d\) formulas by some depth \(d-1\) formulas, the base case being dealt with separately. The key point is a combinatorial lemma similar to the switching lemma used by Hastad. The authors also mention the open problem whether the weak \(\text{PHP}_ n\) (there is no \(1-1\) map of \([2n]\) to \([n]\)) has constant-depth proofs of polynomial size. The main result of the paper was independently obtained by Krajíček, Pudlák and Woods.