A new proof of the weak pigeonhole principle

Abstract

The exact complexity of the weak pigeonhole principle is an old and fundamental problem in proof complexity. Using a diagonalization argument, J. B. Paris et al. (J. Symbolic Logic 53 (1988), 1235-1244) showed how to prove the weak pigeonhole principle with bounded-depth, quasipolynomialsize proofs. Their argument was further refined by J. Krajíček (J. Symbolic Logic 59 (1994), 73-86). In this paper, we present a new proof: we show that the weak pigeonhole principle has quasipolynomial-size LK proofs where every formula consists of a single AND/OR of polylog fan-in. Our proof is conceptually simpler than previous arguments, and is optimal with respect to depth. © 2002 Elsevier Science (USA).