2018/11/10 by Iddo Tzameret, Tzameret, Iddo, Stephen A. Cook +1
Computer Science · Mathematics · #03F20 #03F30 #68Q15 #68Q17 #Computational Complexity (cs.CC) #F.2.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #acm:03F20 #acm:03F30 #acm:68Q15 #acm:68Q17 #cs.CC #cs.LO #math.LO #msc:03F20 #msc:03F30 #msc:68Q15 #msc:68Q17
paper · pdf · doi:10.48550/arxiv.1811.04313
76 pages
arxiv created 2018/11/10 · arxiv updated 2018/11/13
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 Hrubes-Tzameret [SICOMP'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(log 2 n)-depth. This also establishes the existence of uniform polynomial-size NC2-Frege proofs of the basic determinant identities over the integers (previous propositional proofs hold only over the two element field).