Weak theories of linear algebra (Q1766923)

Linear algebra is considered as a source for hard tautologies separating the Frege and Extended Frege propositional proof systems. In his previous works, the second author studied this problem, particularly the question of whether commutativity of matrix inverses has polysize Frege proof, by providing three weak formal theories; the first covering the basic ring properties of matrices, the second extending it with a new function to manipulate matrix powering, and the third in addition enjoying induction on formulas with bounded universal matrix quantifiers. This paper investigates the theories in more detail. The authors give sentences separating quantified versions of these theories. The above-mentioned commutativity of inverses, which has been shown to be provable in the third theory, is shown to be provable even in such a fragment that is obtained by extending the first by allowing induction on formulas with bounded existential matrix quantifiers. The fragment is also shown to be powerful enough to interpret a weak theory \(V^1\) of bounded arithmetic in it and to carry out polynomial-time reasoning about matrices. Thus, for example, one can formulize the Gaussian elimination algorithm in it.