Proving properties of matrices over \({\mathbb{Z}_{2}}\) (Q453198)

This article examines properties of matrices of \(\mathbb{Z}_2\). By proving several matrix properties in weak theories of linear algebra the paper presents a formal approach to linear algebra based on algebraic manipulations according to the ring axioms. This line of research contributes to the programme of reverse mathematics in that it identifies very weak logical theories capable of formalising linear algebra. The second and main motivation for this research comes from proof complexity where the matrix identities \(AB=I \to BA=I\) had been suggested to yield hard candidate formulas for Frege systems. However, after publication of the article under review, \textit{P. Hrubeš} and \textit{I. Tzameret} have shown that these formulas admit quasipolynomial-size Frege proofs [``Short proofs for the determinant identities'', in: Proceedings of the 44th symposium on theory of computing, STOC '12. New York, NY: ACM Press. 193--212 (2012; \url{doi:10.1145/2213977.2213998})]. Still no non-trivial lower bounds are known for Frege systems, and this is one of the major open problems in proof complexity.