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.

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

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.