Speaker: Alasdair Urquhart, University of Toronto

Title: Matrix identities and the pigeonhole principle

Abstract:
We show that short bounded-depth Frege proofs of matrix identities, such
as $PQ=I\supset 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.