We use results from the theory of algebras with polynomial identities (PI algebras) to study the witness complexity of matrix identities. A matrix identity of $d$ by $d$ matrices over a field $\mathbb{F}$ is a non-commutative polynomial $f(x_1,\ldots,x_n)$ over $\mathbb{F}$, such that $f$ vanishes on every $d\times d$ matrix assignment to its variables. For any field $\mathbb{F}$ of characteristic 0, any $d>2$ and any finite basis of $d\times s$ matrix identities over $\mathbb{F}$, we show there exists a family of matrix identities $(f_n)_{n\in\mathbb{N}}$, such that each $f_n$ has $2n$ variables and requires at least $\Omega(n^{2d})$ many generators to generate, where the generators are substitution instances of elements from the basis. The lower bound argument uses fundamental results from PI algebras together with a generalization of the arguments in Hrubes (2011).

We apply this result in algebraic proof complexity, focusing on proof systems for polynomial identities (PI proofs) which operate with algebraic circuits and whose axioms are the polynomial-ring axioms (Hrubes-Tzameret (2009, 2015)), and their subsystems. We identify a decreasing in strength hierarchy of subsystems of PI proofs, in which the $d$th level is a sound and complete proof system for proving $d\times d$ matrix identities (over a given field). For each level $d>2$ in the hierarchy, we establish an $\Omega(n^{2d})$ lower bound on the number of proof-steps needed to prove certain identities.

Finally, we present several concrete open problems about non-commutative algebraic circuits and speed-ups in proof complexity, whose solution would establish stronger size lower bounds on PI proofs of matrix identities, and beyond.

Yet another much improved and slightly more concise exposition, discussion, and motivations. Fix some errors/typos.

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 \times d$ matrices over a field $\mathbb{F}$, is a non-commutative polynomial $f(x_1,\ldots,x_n)$ over $\mathbb{F}$ such that $f$ vanishes on every $d \times 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 [HT12]). We introduce a decreasing in strength hierarchy of proof systems within arithmetic proofs, in which the $d$th level is a sound and complete proof system for proving $d \times 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 $f_n$ with $n$ variables, such that any proof of $f_n=0$ requires $\Omega(n^{2d})$ number of lines.

The lower bound argument uses fundamental results from the theory of algebras with polynomial identities together with a generalization of the arguments in [Hru11]. Specifically, we establish an unconditional lower bound on the minimal number of generators needed to generate a matrix identity, where the generators are substitution instances of elements from any given finite basis of the matrix identities; a result that might be of independent interest.

We then set out to study matrix identities as hard instances for (full) arithmetic proofs. We present two conjectures, one about non-commutative arithmetic circuit complexity and the other about proof complexity, under which up to exponential-size lower bounds on arithmetic proofs (in terms of the arithmetic circuit size of the identities proved) hold. Finally, we discuss the applicability of our approach to strong propositional proof systems such as Extended Frege.

Substantial improvements to the exposition.

We study the complexity of generating identities of matrix rings. We establish an unconditional lower bound on the minimal number of generators needed to generate a matrix identity, where the generators are substitution instances of elements from any given finite basis of the matrix identities. Based on our findings, we propose to consider matrix identities (and their encoding) as hard instances for strong proof systems, and we initiate this study under different settings and assumptions. We show that this direction, under certain conditions, can potentially lead up to exponential-size lower bounds 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). We also discuss shortly the applicability of our approach to strong propositional proof systems.

Formally, the algebraic problem we study is this: for a field $\mathbb{F}$ let $A$ be a non-commutative (associative) $\mathbb{F}$-algebra (e.g., the algebra Mat$_d(\mathbb{F})\;$ of $d\times d$ matrices over $\mathbb{F}$). We say that a non-commutative polynomial $f(x_1,\ldots,x_n)\ \ $ over $\ \mathbb{F}$ is an identity of $A$, if for all $\overline c\in A^n$, $f(\overline c)=0$. Let $B$ be a set of non-commutative polynomials that forms a basis for the identities of $A$, in the following sense: for every identity $f$ of $A$ there exist non-commutative polynomials $g_1,\ldots,g_k$, for some $k$, that are substitution instances of polynomials from $B$, such that $f$ is in the (two-sided) ideal $\langle g_1,\ldots,g_k \rangle$. We study the following question: Given $A,B$ and $f$ as above, what is the minimal number $k$ of such generators $g_1,\ldots,g_k\ $ for which $\ f\in \langle g_1,\ldots,g_k \rangle\ $ ?
In particular, we focus on the case where the algebra $A$ is Mat$_d(\mathbb{F})$, and $\mathbb{F}$ has characteristic $0$. Our main technical contribution is a generalization of the lower bound presented in Hrubes (2011) (for the case $d=1$) to any $d>2$:

For every natural number $d>2$ and every finite basis $B$ for the identities of Mat$_d(\mathbb{F})$, where $\mathbb{F}$ is of characteristic $0$, there exists an identity $f_n$ with $n$ variables, that requires $\Omega(n^{2d})$ generators (i.e., substitution instances from $B$) to generate.

The proof uses fundamental results from the theory of algebras with polynomial identities (PI-algebras) together with a generalization of the arguments in \cite{Hru11}.

Improvements to exposition. Changed title.

Motivated by the fundamental lower bounds questions in proof complexity, we investigate the complexity of generating identities of matrix rings, and related problems. Specifically, for a field $\mathbb{F}$ let $A$ be a non-commutative (associative) $\mathbb{F}$-algebra (e.g., the algebra Mat$_d(\mathbb{F})\;$ of $d\times d$ matrices over $\mathbb{F}$). We say that a non-commutative polynomial $f(x_1,\ldots,x_n)\ \ $ over $\ \mathbb{F}$ is an identity of $A$, if for all $\overline c\in A^n$, $f(\overline c)=0$. Let $B$ be a set of non-commutative polynomials that forms a basis for the identities of $A$, in the following sense: for every identity $f$ of $A$ there exist non-commutative polynomials $g_1,\ldots,g_k$, for some $k$, that are substitution instances of polynomials from $B$, such that $f$ is in the (two-sided) ideal $\langle g_1,\ldots,g_k \rangle$. We study the following question: Given $A,B$ and $f$ as above, what is the minimal number $k$ of such generators $g_1,\ldots,g_k\ $ for which $\ f\in \langle g_1,\ldots,g_k \rangle\ $ ?

In particular, we focus on the case where the algebra $A$ is Mat$_d(\mathbb{F})$, and $\mathbb{F}$ has characteristic $0$. Our main technical contribution is a generalization of the lower bound presented in Hrubes (2011) (for the case $d=1$) to any $d>2$:

For every natural number $d>2$ and every finite basis $B$ for the identities of Mat$_d(\mathbb{F})$, where $\mathbb{F}$ is of characteristic $0$, there exists an identity $f_n$ with $n$ variables, that requires $\Omega(n^{2d})$ generators (i.e., substitution instances from $B$) to generate.

Note that for any $d>2$, it is an open problem to find a basis for the identities of Mat$_d(\mathbb{F})$ (while the existence of a finite basis was proved by Kemer (1987)). Nevertheless, using results from the theory of algebras with polynomial identities (PI-algebras) together with a generalization of the arguments in Hrubes (2011), we conclude the above lower bound for every finite basis $B$.

We then explore connections to lower bounds in proof complexity. We consider arithmetic proofs of polynomial identities that operate with algebraic circuits and whose axioms are the polynomial-ring axioms (which can be considered as an algebraic analogue of the Extended Frege propositional proof system). We raise the following basic question: is it true that using the generators of the (non-commutative) polynomial identities over Mat$_d(\mathbb{F})$ as axiom (schemes) is an optimal way to prove such identities, with respect to proof size? Namely, is it true that proving matrix identities by reasoning with polynomials whose variables $X_1,\ldots, X_n$ range over matrices is as efficient as proving matrix identities using polynomials whose variables range over the *entries* of the matrices $X_1,\ldots, X_n$? We show that a positive answer to this question may lead, under further assumptions (which are generalization of the assumptions presented in Hrubes (2011)), up to exponential-size lower bounds on arithmetic proofs.