In this talk, we discuss and relate the frameworks for representing complexity classes appearing in descriptive complexity and bounded arithmetic (proof complexity). We show what is needed for the descriptive complexity of formulas to determine exactly their proving power. That is, we describe how the knowledge of the expressive power of a class of formulas can be used to construct a system of bounded arithmetic capturing the corresponding complexity class. We apply this method to characterize several classes of efficiently computable functions such as functions computable in P and NL. We will also discuss the problem of formalizing combinatorial principles in systems of arithmetic, and other applications of this framework.
Most of the results presented here are joint work with Stephen Cook.
Antonina Kolokolova obtained her PhD from the University of Toronto in 2005, under the supervision of Stephen Cook. She then was a postdoc at the Mathematical Institute of the Czech Academy of Sciences, Prague. Now she is a postdoc at Simon Fraser University. Her main research interests are in logic and complexity, especially in the fields of bounded arithmetic and descriptive complexity.