Linear algebra in weak formal theories of arithmetic
Iddo Tzameret ( Royal Holloway, University of London )

14:00 22nd February 2018 ( week 6, Hilary Term 2018 )Tony Hoare Room  Robert Hooke Building
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/computationalcomplexity 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.