The complexity of the pigeonhole principle

The pigeonhole principle for n is the statement that there is no one-to-one function between a set of size n and a set of size n-1. This statement can be formulated as an unlimited-fan-in constant depth polynomial-size Boolean formula PHP_n in n(n-1) variables, PHP_n can be proved in the propositional calculus; that is, a sequence of Boolean formulas can be given so that each one is either an axiom of the propositional calculus or a consequence of some of the previous ones according to an inference rule of the propositional calculus, the last one being PHP_n. The main result is that the pigeonhole principle cannot be proved in this way if the size of the proof (the total number or symbols of the formulas in the sequence) is polynomial in n and each formula is constant-depth (unlimited-fan-in), polynomial size and contains only the variables of PHP_n