The proof theoretic strength of the Steinitz exchange theorem Original Research Article

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