Matrix identities and the pigeonhole principle

Abstract.We show that short bounded-depth Frege proofs of matrix identities, such as PQ=I⊃QP=I (over the field of two elements), imply short bounded-depth Frege proofs of the pigeonhole principle. Since the latter principle is known to require exponential-size bounded-depth Frege proofs, it follows that the propositional version of the matrix principle also requires bounded-depth Frege proofs of exponential size.