Tuesday 23 November 2010
2:30 - 4:00   Phuong The Nguyen
Bounded arithmetic and bounded reverse mathematics

Abstract In bounded arithmetic complexity classes are associated with first-order theories that are weak fragments of Peano arithmetic. Associated with the polynomial hierarchy are Buss's theories in the hierarchy S2, while for classes below polytime the theories are developed using Zambella's elegant two-sorted syntax. Reasoning in a theory of bounded arithmetic can be said to use only concepts of the associated complexity class. The goal of bounded reverse mathematics is to formalize proofs of mathematical theorems in the weakest possible theory of bounded arithmetic. In other words, we try to find proofs that use concepts of smallest possible complexity. In this talk I will introduce theories of bounded arithmetic and briefly mention some problems in bounded reverse mathematics. The theories of bounded arithmetic can also be seen as uniform version of various propositional proof systems, but this connection is beyond the scope of the talk.