Bounded Arithmetic and Propositional Proof Complexity
This is a survey of basic facts about bounded arithmetic and about the relationships between bounded arithmetic and propositional proof complexity. We introduce the theories and of bounded arithmetic and characterize their proof theoretic strength and their provably total functions in terms of the polynomial time hierarchy. We discuss other axiomatizations of bounded arithmetic, such as minimization axioms. It is shown that the bounded arithmetic hierarchy collapses if and only if bounded arithmetic proves that the polynomial hierarchy collapses.