Weak theories of linear algebra (Q1766923)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Weak theories of linear algebra |
scientific article |
Statements
Weak theories of linear algebra (English)
0 references
2 March 2005
0 references
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.
0 references
linear algebra
0 references
complexity of proofs
0 references
Frege propositional proof system
0 references
polysize Frege proof
0 references
polynomial time reasoning
0 references
commutativity of matrix inverse
0 references
bounded arithmetic
0 references
Gaussian elimination algorithm
0 references