The purpose of this paper is to survey the correspondence between bounded arithmetic and propositional proof systems. In addition, it also contains some new results which have appeared as an extended abstract in the proceedings of the conference TAMC 2008 [11].Bounded arithmetic is closely related to propositional proof systems; this relation has found many fruitful applications. The aim of this paper is to explain and develop the general correspondence between propositional proof systems and arithmetic theories, as introduced by Krajíček and (...) Pudlák [46]. Instead of focusing on the relation between particular proof systems and theories, we favour a general axiomatic approach to this correspondence. In the course of the development we particularly highlight the role played by logical closure properties of propositional proof systems, thereby obtaining a characterization of extensions of EF in terms of a simple combination of these closure properties (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

Let g be a map defined as the Nisan–Wigderson generator but based on an NP ∩ coNP -function f. Any string b outside the range of g determines a propositional tautology τb expressing this fact. Razborov [27] has conjectured that if f is hard on average for P/poly then these tautologies have no polynomial size proofs in the Extended Frege system EF. We consider a more general Statement that the tautologies have no polynomial size proofs in any propositional proof system. (...) This is equivalent to the statement that the complement of the range of g contains no infinite NP set. We prove that Statement is consistent with Cook' s theory PV and, in fact, with the true universal theory T PV in the language of PV. If PV in this consistency statement could be extended to "a bit" stronger theory then Razborov's conjecture would follow, and if TPV could be added too then Statement would follow. We discuss this problem in some detail, pointing out a certain form of reflection principle for propositional logic, and we introduce a related feasible disjunction property of proof systems. (shrink)

We consider exponentially large finite relational structures (with the universe {0.1}ⁿ) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that: 1. If there exists a P/poly map g: {0.1} → {0.1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in (...) a size 2ⁿ tournament is hard for the proof system. 2. The search problem WPHP, decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph. Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems. (shrink)