Weak theories of linear algebra

Abstract. We investigate the theories LA, LAP, LAP 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 LA of LAP in which we can interpret a weak theory V 1 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, LA proves the commutativity of inverses.

• Type: Journal
• Year: 2005
• Where: AML
• Authors: Neil Thapen, Michael Soltys
• Keywords: AML 2005, Frege Proofs, Matrix Inverses, Theories La