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 …