We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.

Pudlák shows that bounded arithmetic proves an upper bound on the Ramsey number Rr . We will strengthen this result by improving the bound. We also investigate lower bounds, obtaining a non-constructive lower bound for the special case of 2 colors , by formalizing a use of the probabilistic method. A constructive lower bound is worked out for the case when the monochromatic set size is fixed to 3 . The constructive lower bound is used to prove two “reversals”. To (...) explain this idea we note that the Ramsey upper bound proof for k=3 uses the weak pigeonhole principle in a significant way. The Ramsey upper bound proof for the case in which the upper bound is not explicitly mentioned, uses the totality of the exponentiation function in a significant way. It turns out that the Ramsey upper bounds actually imply the respective principles used to prove them, indicating that these principles were in some sense necessary. (shrink)

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)

We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular logics, all logics (...) of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result. (shrink)

We study the long-standing open problem of giving$\forall {\rm{\Sigma }}_1^b$separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the$\forall {\rm{\Sigma }}_1^b$Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole (...) principle for FPNPfunctions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of$T_2^1$augmented with the surjective weak pigeonhole principle for polynomial time functions. (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 develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [15]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV₁ + dWPHP(PV).

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK . We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.

We look for a converse to a result from [N. Thapen, A model-theoretic characterization of the weak pigeonhole principle, Annals of Pure and Applied Logic 118 175–195] that if the weak pigeonhole principle fails in a model K of bounded arithmetic, then there is an end-extension of K interpretable inside K. We show that if a model J of an induction-free theory of arithmetic is interpretable inside K, then either J is isomorphic to an initial segment of K , or (...) K is isomorphic to an initial segment of J and in this case the weak pigeonhole principle fails in K. This result is formulated in terms of a theory of bounded arithmetic with a greatest element. We go on to consider structures defined by oracles, and use the probabilistic witnessing theorem for to give a general criterion for what can be proved about these using the weak pigeonhole principle. We also show that the injective WPHP is not provable in this theory in the relativized case. (shrink)

It is well known that S12 cannot prove the injective weak pigeonhole principle for polynomial time functions unless RSA is insecure. In this note we investigate the provability of the surjective weak pigeonhole principle in S12 for provably weaker function classes.