References

It is well-known that theories of Bounded Arithmetic are closely related to propositional proof systems. This relation can be utilized in both direc-tions: upper bounds and simulations for propositional proof systems can be shown by constructing proofs in the corresponding theories, and indepen-dence results for certain theories can be proven via lower bounds on the length of propositional proofs. This survey paper explains and develops the general correspondence be-tween propositional proof systems and arithmetic theories, as introduced by Kraj́ıček and Pudlák [1]. Instead of focussing on particular pairs of proof systems and theories, a general axiomatic approach to the correspondence is presented. A particularly emphasis is put on the role played by logical closure properties of propositional proof systems. This also yields a new characterization of extensions of Extended Frege systems in terms of simple combinations of these closure properties