E.Jerabek's tutorial at the
Fall school (Sept.'11)

Bounded arithmetic

---

Bounded arithmetic is a collective name for a family of weak axiomatic theories based on integer arithmetic that include the schema of induction (or other schemata used in their axiom systems) only for (a subset of) bounded formulas, and that do not prove the totality of the exponential function. While it originally arose from the study of fragments of Peano arithmetic, bounded arithmetic is closely connected to fundamental problems in propositional proof complexity and computational complexity. The aim of this tutorial is to provide a basic introduction to bounded arithmetic.

The tentative schedule is as follows:

Talk 1: Overview and motivation. Buss’s theories S₂ⁱ, T₂ⁱ: definitions and basic properties.

Talk 2: Provably total computable functions and witnessing theorems – Parikh’s theorem, Buss’s witnessing theorem, KPT witnesing theorem.

Talk 3: Second-order bounded arithmetic – theories Vⁱ, the RSUV isomorphism, theories for small complexity classes.

Talk 4: Propositional proof systems, reflection principles, propositional translations of bounded formulas.

Recommended reading

[1] S. Buss, Bounded arithmetic, Bibliopolis, Naples, 1986, revision of 1985 Princeton University Ph.D. thesis.

[2] J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications vol. 60, Cambridge University Press, 1995.

[3] S. Cook and P. Nguyen, Logical foundations of proof complexity, Cambridge University Press, New York, 2010.

[4] P. Hájek and P. Pudlák, Metamathematics of first-order arithmetic, Chapter V, Springer, 1993, second edition 1998.