Formal Theories for Linear Algebra

TL;DR

This paper develops formal logical theories for complexity classes related to linear algebra, specifically L and DET, and connects them to existing linear algebra theories over various domains.

Contribution

It introduces two-sorted theories for L and DET, and interprets Soltys' linear algebra theory within these, establishing formal proof equivalences.

Findings

Standard linear algebra theorems over Z2 and Z are provable in the theories.

Theories correspond to complexity classes L and DET.

Open question remains on proving the theorems themselves.

Abstract

We introduce two-sorted theories in the style of [CN10] for the complexity classes \oplusL and DET, whose complete problems include determinants over Z2 and Z, respectively. We then describe interpretations of Soltys' linear algebra theory LAp over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over Z2 and Z can be proved in the corresponding theory, but leaves open the interesting question of whether the theorems themselves can be proved.