Matrix identities and the pigeonhole principle

We show that short bounded-depth Frege proofs of matrix identities, such as P Q = 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.

• Type: Journal
• Year: 2004
• Where: AML
• Authors: Michael Soltys, Alasdair Urquhart
• Keywords: AML 2004, Bounded-depth Frege Proofs, Matrix Identities, Short Bounded-depth Frege