Weak theories of linear algebra
type: Item
instance of: scholarly article
title: Weak theories of linear algebra
zbMATH Open document ID: 1064.03037
author: Neil Thapen
author: Michael Soltys
published in: Archive for Mathematical Logic
publication date: 2005-03-02T00:00:00Z
review text: 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.
reviewed by: Osamu Sonobe
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 15A24
Mathematics Subject Classification ID: 15A27
zbMATH DE Number: 2140314
zbMATH Keywords: linear algebra
zbMATH Keywords: complexity of proofs
zbMATH Keywords: Frege propositional proof system
zbMATH Keywords: polysize Frege proof
zbMATH Keywords: polynomial time reasoning
zbMATH Keywords: commutativity of matrix inverse
zbMATH Keywords: bounded arithmetic
zbMATH Keywords: Gaussian elimination algorithm
MaRDI profile type: Publication
full work available at URL: s00153-004-0249-8
OpenAlex ID: W1987241097
cites work: On computing the determinant in small parallel time using a small number of processors
cites work: Q4850545
cites work: Q3794177
cites work: A taxonomy of problems with fast parallel algorithms
cites work: Q4003421
cites work: The proof complexity of linear algebra
cites work: Notes on polynomially bounded arithmetic
DOI: 10.1007/S00153-004-0249-8
description: scientific article; zbMATH DE number 2140314