Journal article:
Samuel R. Buss.
"Polynomial Size Proofs of the Propositional Pigeonhole
Principle."
Journal of Symbolic Logic 52, no. 4 (1987) 916-927 .
Download journal article: searchable PDF or plain PDF.
Abstract Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic..