Linear algebra in weak formal theories of arithmetic

Abstract:

I will demonstrate how one can prove and develop basic linear algebra in what is apparently the weakest formal theory of arithmetic possible.
This aligns with the direction of research that attempts to bridge the gap between the computational complexity of functions and the logical/computational-complexity of concepts required to prove basic statements about the functions. In our case, we show that to prove basic properties of the determinant function it is enough to reason with concepts of the same complexity class that can compute the determinant function. 

Joint work with Stephen Cook.