Uniform, Integral, and Feasible Proofs for the Determinant Identities
- 13 January 2021
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 68 (2), 1-80
- https://doi.org/10.1145/3431922
Abstract
Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubeš-Tzameret [15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory VNC2; the latter is a first-order theory corresponding to the complexity class NC2 consisting of problems solvable by uniform families of polynomial-size circuits and O(log2 n)-depth. This also establishes the existence of uniform polynomial-size propositional proofs operating with NC2-circuits of the basic determinant identities over the integers (previous propositional proofs hold only over the two-element field).Keywords
Funding Information
- National Natural Science Foundation of China (61373002)
This publication has 26 references indexed in Scilit:
- Formal Theories for Linear AlgebraLogical Methods in Computer Science, 2012
- A sorting network in bounded arithmeticAnnals of Pure and Applied Logic, 2011
- Arithmetic Circuits: A survey of recent results and open questionsFoundations and Trends® in Theoretical Computer Science, 2009
- The proof complexity of linear algebraAnnals of Pure and Applied Logic, 2004
- Dual weak pigeonhole principle, Boolean complexity, and derandomizationAnnals of Pure and Applied Logic, 2004
- Non-commutative arithmetic circuits: depth reduction and size lower boundsTheoretical Computer Science, 1998
- Counting problems in bounded arithmeticLecture Notes in Mathematics, 1985
- On computing the determinant in small parallel time using a small number of processorsInformation Processing Letters, 1984
- Fast Probabilistic Algorithms for Verification of Polynomial IdentitiesJournal of the ACM, 1980
- Existence and feasibility in arithmeticThe Journal of Symbolic Logic, 1971