Short Proofs for the Determinant Identities

We study arithmetic proof systems ${\mathbb P}_c({\mathbb F})$ and $ {\mathbb P}_f({\mathbb F})$ operating with arithmetic circuits and arithmetic formulas, respectively, and 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) $ in which every circuit has depth $ O(k+\log^2 d + \log d\cdot \log s) $. As a corollary, we obtain a quasi-polynomial simulation of ${\mathbb P}_c({\mathbb F})$ by ${\mathbb P}_f({\mathbb F})$. Using these results we obtain the following: consider the identities $\det(XY) = \det(X)\cdot\det(Y) \mbox{ and } \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 using circuits of $ 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 $\mathbf{NC}^2$-Frege proofs for the determinant identities and the hard matrix identities, as considered, e.g., in Soltys and Cook [Ann. Pure Appl. Logic, 130 (2004), pp. 277--323] (cf. Beame and Pitassi [Bull. Eur. Assoc. Theor. Comput. Sci. EATCS, 65 (1998), pp. 66--89]). 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 $\mathbf{NC}^2$-Frege proofs and quasi-polynomial-size Frege proofs.