We study arithmetic proof systems Pc(F) and Pf(F) operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field F. We establish a series of structural theorems about these proof systems, the main one stating that Pc(F) proofs can be balanced: if a polynomial identity of syntactic degree d and depth k has a Pc(F) proof of size s, then it also has a Pc(F) proof of size poly(sd) and depth O(k+log2d+logdlogs). As a corollary, we obtain a quasipolynomial simulation of Pc(F) by Pf(F), for identities of a polynomial syntactic degree.

Using these results we obtain the following: consider the identitiesdet(XY)=det(X)det(Y) and det(Z)=z11znnwhere XY and Z are nn square matrices and Z is a triangular matrix with z11znn 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 Pc(F) proofs of polynomial-size and O(log2n) depth. Moreover, there exists an arithmetic formula det of size nO(logn) such that the above identities have Pf(F) proofs of size nO(logn).

This yields a solution to a basic open problem in propositional proof complexity, namely, whether there are polynomial-size NC2-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=IBA=I (for matrices over the two element field) as well as basic properties of the determinant have polynomial-size NC2-Frege proofs, and quasipolynomial-size Frege proofs.