The proof theoretic strength of the Steinitz exchange theorem

We show that the logical theory QLA proves the Cayley–Hamilton theorem from the Steinitz exchange theorem together with a strengthening of the linear independence principle. Since QLA is a fairly weak theory (in the sense that its quantifier-free fragment, LA, translates into tautologies with TC0-Frege proofs—when restricted to the field Q of the rationals), it follows that the proof complexity of matrix algebra can be distilled to the Steinitz exchange theorem. © 2006 Elsevier B.V. All rights reserved.

• Type: Journal
• Year: 2007
• Where: DAM
• Authors: Michael Soltys
• Keywords: DAM 2007, Linear Independence Principle, Logical Theory Qla, Steinitz Exchange Theorem