| In this thesis we are concerned with building logical foundations for Linear Algebra, from the perspective of proof complexity. As the cornerstone of our logical theories, we use Berkowitz's parallel algorithm for computing the coefficients of the characteristic polynomial of a matrix.; Standard Linear Algebra textbooks use Gaussian Elimination as the main algorithm, but they invariably use the (very infeasible) Lagrange expansion to prove properties of this algorithm.; The main contribution of this thesis is a (first) feasible proof of the Cayley-Hamilton Theorem, and related principles of Linear Algebra (namely, the axiomatic definition of the determinant, the cofactor expansion formula, and multiplicativity of the determinant). Furthermore, we show that these principles are equivalent, and the equivalence can be proven feasibly.; We also show that a large class of matrix identities, such as: AB=I→BA=I proposed by S. A. Cook as a candidate for separating Frege and Extended Frege propositional proof systems, all have feasible proofs, and hence polynomially-bounded Extended Frege proofs. We introduce the notion of completeness for these matrix identities.; As the main tool to prove our results, we design three logical theories: LA⊂ LAP⊂ ∀LAP LA is a three-sorted quantifier-free theory of Linear Algebra. The three sorts are indices, field elements and matrices. This is a simple theory that allows us to formalize and prove all the basic properties of matrices (roughly the properties that state that the set of matrices is a ring). The theorems of LA have polynomially-bounded Frege proofs.; We extend LA to LAP by adding a new function, P, which is intended to denote matrix powering, i.e., P( n, A) means An. LAP is well suited for formalizing Berkowitz's algorithm, and it is strong enough to prove the equivalence of some fundamental principles of Linear Algebra. The theorems of LAP translate into quasi-polynomially-bounded Frege proofs.; We finally extend LAP to ∀LAP by allowing induction on formulas with ∀ matrix quantifiers. This new theory is strong enough to prove the Cayley-Hamilton Theorem, and hence (by our equivalence) all the major principles of Linear Algebra. The theorems of ∀LAP translate into polynomially-bounded Extended Frege proofs. |
