Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Revision(s):

Revision #1 to TR11-174 | 22nd April 2013 13:07

#### Short Proofs for the Determinant Identities

Revision #1
Authors: Pavel Hrubes, Iddo Tzameret
Accepted on: 22nd April 2013 13:07
Downloads: 1954
Keywords:

Abstract:

We study arithmetic proof systems $\mathbb{P}_c(\mathbb{F})$ and $\mathbb{P}_f(\mathbb{F})$ operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field $\mathbb{F}$. We establish a series of structural theorems about these proof systems, the main one stating that $\mathbb{P}_c(\mathbb{F})$ proofs can be balanced: if a polynomial identity of syntactic degree $d$ and depth $k$ has a $\mathbb{P}_c(\mathbb{F})$ proof of size $s$, then it also has a $\mathbb{P}_c(\mathbb{F})$ proof of size ${\rm poly}(s,d)$ and depth $O(k+\log^2 d + \log d\cdot \log s)$. As a corollary, we obtain a quasipolynomial simulation of $\mathbb{P}_c(\mathbb{F})$ by $\mathbb{P}_f(\mathbb{F})$, for identities of a polynomial syntactic degree.

Using these results we obtain the following: consider the identities
$\det(XY) = \det(X)\cdot\det(Y) \quad\mbox{ and }\quad \det(Z)= z_{11}\cdots z_{nn},$
where $X,Y$ and $Z$ are $n\times n$ square matrices and $Z$ is a triangular matrix with $z_{11},\dots, z_{nn}$ on the diagonal (and $\det$ is the determinant polynomial). Then we can construct a polynomial-size arithmetic circuit $\det$ such that the above identities have $\mathbb{P}_c(\mathbb{F})$ proofs of polynomial-size and $O(\log^2 n)$ depth. Moreover, there exists an arithmetic formula $\det$ of size $n^{O(\log n)}$ such that the above identities have $\mathbb{P}_f(\mathbb{F})$ proofs of size $n^{O(\log n)}$.

This yields a solution to a basic open problem in propositional proof complexity, namely, whether there are polynomial-size $NC^2$-Frege proofs for the determinant identities and the \emph{hard matrix identities}, as considered, e.g.~in Soltys and Cook (2004) (cf., Beame and Pitassi (1998)). We show that matrix identities like $AB=I \rightarrow BA=I$ (for matrices over the two element field) as well as basic properties of the determinant have polynomial-size $NC^2$-Frege proofs, and quasipolynomial-size Frege proofs.

Changes to previous version:

Revision and corrections to Section 7. Addition of short proofs for the Cayley-Hamilton theorem. Other minor changes.

### Paper:

TR11-174 | 30th December 2011 10:58

#### Short Proofs for the Determinant Identities

TR11-174
Authors: Pavel Hrubes, Iddo Tzameret
Publication: 30th December 2011 14:49
Downloads: 2869
Keywords:

Abstract:

We study arithmetic proof systems $\mathbb{P}_c(\mathbb{F})$ and $\mathbb{P}_f(\mathbb{F})$ operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field $\mathbb{F}$. We establish a series of structural theorems about these proof systems, the main one stating that $\mathbb{P}_c(\mathbb{F})$ proofs can be balanced: if a polynomial identity of syntactic degree $d$ and depth $k$ has a $\mathbb{P}_c(\mathbb{F})$ proof of size $s$, then it also has a $\mathbb{P}_c(\mathbb{F})$ proof of size ${\rm poly}(s,d)$ and depth $O(k+\log^2 d + \log d\cdot \log s)$. As a corollary, we obtain a quasipolynomial simulation of $\mathbb{P}_c(\mathbb{F})$ by $\mathbb{P}_f(\mathbb{F})$, for identities of a polynomial syntactic degree.

Using these results we obtain the following: consider the identities
$\det(XY) = \det(X)\cdot\det(Y) \quad\mbox{ and }\quad \det(Z)= z_{11}\cdots z_{nn},$
where $X,Y$ and $Z$ are $n\times n$ square matrices and $Z$ is a triangular matrix with $z_{11},\dots, z_{nn}$ on the diagonal (and $\det$ is the determinant polynomial). Then we can construct a polynomial-size arithmetic circuit $\det$ such that the above identities have $\mathbb{P}_c(\mathbb{F})$ proofs of polynomial-size and $O(\log^2 n)$ depth. Moreover, there exists an arithmetic formula $\det$ of size $n^{O(\log n)}$ such that the above identities have $\mathbb{P}_f(\mathbb{F})$ proofs of size $n^{O(\log n)}$.

This yields a solution to a long-standing open problem in propositional proof complexity, namely, whether there are polynomial-size $NC^2$-Frege proofs for the determinant identities and the \emph{hard matrix identities}, as considered, e.g.~in Soltys and Cook (2004) (cf., Beame and Pitassi (1998)). We show that matrix identities like $AB=I \rightarrow BA=I$ (for matrices over the two element field) as well as basic properties of the determinant have polynomial-size $NC^2$-Frege proofs, and quasipolynomial-size Frege proofs.

ISSN 1433-8092 | Imprint