LA, Permutations, and the Hajós Calculus

LA is a simple and natural field independent system for reasoning about matrices. We show that LA extended to contain a matrix form of the pigeonhole principle is strong enough to prove a host of matrix identities (so called “hard matrix identities” which are candidates for separating Frege and extended Frege). LAP is LA with matrix powering; we show that LAP extended with quantification over permutations is strong enough to prove theorems such as the Cayley-Hamilton Theorem. Furthermore, we show that LA extended with quantification over permutations expresses NP graph-theoretic properties, and proves the soundness of the Hajós calculus. A corollary is that a fragment of Quantified Permutation Frege (a novel propositional proof system that we introduce in this paper) is p-equivalent of extended Frege. Several open problems are stated.