The authors establish a significant extension of Ha˚stad’s switching lemma to the setting of one-to-one mappings and prove an exponential lower bound on the size of constant-depth Frege (propositional) proofs of propositional formulations of the pigeonhole principle. These are the first exponential lower bounds for constant-depth Frege proofs.

The Frege proofs considered in this paper are propositional proofs in the language AND and OR with (possibly negated) variables; the depth of a proof is the maximum alternation of ANDs and ORs in a formula in the proof. PHP _n is a propositional formula encoding the pigeonhole principle on n objects. The primary technical tool of the paper is a “switching lemma,” which states that a suitably random partial one-to-one map acting as a restriction on a formula of depth d + 1 will collapse it to an equivalent formula of depth d. This lemma is applied to show that any depth- d Frege proof requires at least exp( n ^{c d} ) symbols, for some constant c. Furthermore, polynomial-size proofs of PHP _n must have depth &OHgr; ( loglog n ) .