The proof complexity of linear algebra (Q1886325)

The authors analyze the complexity of the concepts needed to prove the basic theorems of linear algebra. One of the important results obtained in this paper is that the Cayley-Hamilton theorem enjoys a feasible proof. The analysis is carried out by making use of three formal theories, each of which is carefully designed so as to examine the basic theorems under a certain complexity, respectively. The basic ring properties of matrices, for example, are covered by the first theory whose theorems translate into tautology families with polynomial size Frege proofs. The theory proves also the equivalence between some principles called hard matrix identities such as \(AB = I\) iff \(BA = I\) for which it is usually required to compute inverses. The second theory, which is an extension of the first with a new function to manipulate matrix powering, proves that the C-H theorem not only implies the hard matrix identities but also is equivalent to such principles as axiomatic definition of det and cofactor expansion, respectively. Finally the third theory is based on the second by allowing induction on formulas with bounded universal matrix quantifiers, so that the major principles of linear algebra including the C-H theorem are all provable in it. After these observations, the authors show how the theories are translated into propositional proof systems of certain complexities, respectively, with which the complexities of the proofs of the considered principles are determined explicitly.