Short Proofs for the Determinant Identities

TL;DR

This paper develops structural theorems for arithmetic proof systems proving polynomial identities, enabling polynomial-size proofs for determinant identities and matrix properties within certain proof systems.

Contribution

It introduces a quasipolynomial simulation of P_c(F) by P_f(F) and constructs polynomial-size proofs for key determinant and matrix identities in propositional proof systems.

Findings

P_c(F) proofs can be balanced with poly(s,d) size and logarithmic depth.

Polynomial-size proofs for determinant identities in P_c(F) and P_f(F).

Polynomial-size NC^2-Frege proofs for determinant and matrix identities.

Abstract

We study arithmetic proof systems P_c(F) and P_f(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 P_c(F) proofs can be balanced: if a polynomial identity of syntactic degree d and depth k has a P_c(F) proof of size s, then it also has a P_c(F) proof of size poly(s,d) and depth O(k+\log^2 d + \log d\cd \log s). As a corollary, we obtain a quasipolynomial simulation of P_c(F) by P_f(F), for identities of a polynomial syntactic degree. Using these results we obtain the following: consider the identities det(XY) = det(X)det(Y) and det(Z)= z_{11}... z_{nn}, where X,Y and Z are nxn square matrices and Z is a triangular matrix with z_{11},..., 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 P_c(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 P_f(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 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 {\to} 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.