Generating Matrix Identities and Proof Complexity

Motivated by the fundamental lower bounds questions in proof complexity, we initiate the study of matrix identities as hard instances for strong proof systems. A matrix identity of d × d matrices over a field F, is a non-commutative polynomial f(x1,..., xn) over F such that f vanishes on every d × d matrix assignment to its variables. We focus on arithmetic proofs, which are proofs of polynomial identities operating with arithmetic circuits and whose axioms are the polynomial-ring axioms (these proofs serve as an algebraic analogue of the Extended Frege propositional proof system; and over GF (2) they constitute formally a sub-system of Extended Frege [9]). We introduce a decreasing in strength hierarchy of proof systems within arithmetic proofs, in which the dth level is a sound and complete proof system for proving d × d matrix identities (over a given field). For each level d> 2 in the hierarchy, we establish a proof-size lower bound in terms of the number of variables in the matrix identity proved: we show the existence of a family of matrix identities fn with n variables, such that an