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 *S*_{2},
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.