LA, permutations, and the Hajós Calculus

LA is a simple and natural logical system for reasoning about matrices. We show that LA, over finite fields, proves a host of matrix identities (so-called “hard matrix identities”) from the matrix form of the pigeonhole principle. LAP is LA with matrix powering; we show that LAP extended with quantification over permutations is strong enough to prove fundamental theorems of linear algebra (such as the Cayley–Hamilton Theorem). Furthermore, we show that LA with quantification over permutations expresses NP graph-theoretic properties, and proves the soundness of the Hajós Calculus. Several open problems are stated.