Introduction to bounded arithmetic
Raheleh Jalali
University of Bath
Bounded arithmetic provides a deep connection between proof theory and computational complexity, revealing how weak arithmetic systems can model feasible computation. By restricting induction to bounded formulas, these theories allow us to study the relationship between logical definability and computational efficiency. A key result shows that functions definable in fragments like correspond to natural complexity classes. For instance, provably recursive functions of are exactly those computable in polynomial time. Proof-theoretic techniques, such as cut elimination, play a crucial role here, turning proofs into algorithms. The framework also extends to higher complexity classes like PSPACE and EXPTIME through second-order theories. Beyond its intrinsic logical interest, bounded arithmetic reformulates major open problems (such as P vs. NP) in proof-theoretic terms, offering new perspectives for both fields. This tutorial will explore these ideas, highlighting how formal systems can capture computational phenomena in surprising and elegant ways. There are multiple excellent references on the subject, as listed below.
[1] Buss, Samuel R. Bounded arithmetic. Princeton University, 1985.
[2] Buss, Samuel R. “Bounded arithmetic and propositional proof complexity.”
Logic of computation. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997.
67-121.
[3] Cook, Stephen, and Phuong Nguyen. Logical foundations of proof complexity.
Vol. 31. Cambridge: Cambridge University Press, 2010.
[4] Krajı́ček, Jan. Bounded arithmetic, propositional logic and complexity
theory. Vol. 60. Cambridge University Press, 1995.