Weak theories of linear algebra

We investigate the theories [inline-graphic not available: see fulltext] of linear algebra, which were originally defined to study the question of whether commutativity of matrix inverses has polysize Frege proofs. We give sentences separating quantified versions of these theories, and define a fragment [inline-graphic not available: see fulltext] in which we can interpret a weak theory V1 of bounded arithmetic and carry out polynomial time reasoning about matrices - for example, we can formalize the Gaussian elimination algorithm. We show that, even if we restrict our language, [inline-graphic not available: see fulltext] proves the commutativity of inverses.