Journal of Mathematical Logic, Volume 22, Issue 03, December 2022. We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory [math] of [E. Jeřábek, Approximate counting by hashing in bounded arithmetic, J. Symb. Log. 74(3) (2009) 829–860]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational (...) characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS. As CPLS is provably total in the theory [math], this shows that [math] does not prove every [math] sentence which is provable in bounded arithmetic. This answers the question posed in [S. Buss, L. A. Kołodziejczyk and N. Thapen, Fragments of approximate counting, J. Symb. Log. 79(2) (2014) 496–525] and represents some progress in the program of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences. Our main technical tool is an extension of the “fixing lemma” from [P. Pudlák and N. Thapen, Random resolution refutations, Comput. Complexity, 28(2) (2019) 185–239], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a [math] oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic. (shrink)

A polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory \ of all polynomial time functions. Generalizing a theorem of Hirschfeld :111–126, 1975), we show that every countable model of \ is isomorphic to an existentially closed substructure of a polynomial time ultrapower. Moreover, one can take a substructure of a special form, namely a limit polynomial time ultrapower in the classical sense of Keisler Ultrafilters across (...) mathematics, contemporary mathematics vol 530, pp 163–179. AMS, New York, 1963). Using a polynomial time ultrapower over a nonstandard Herbrand saturated model of \ we show that \ is consistent with a formal statement of a polynomial size circuit lower bound for a polynomial time computable function. This improves upon a recent result of Krajíček and Oliveira, 2017). (shrink)

We give a uniform proof of the theorems of Yao and Beigel–Tarui representing ACC predicates as constant depth circuits with MODm\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {MOD}_{m}$$\end{document} gates and a symmetric gate. The proof is based on a relativized, generalized form of Toda’s theorem expressed in terms of closure properties of formulas under bounded universal, existential and modular counting quantifiers. This allows the main proofs to be expressed in terms of formula classes instead of Boolean circuits. (...) The uniform version of the Beigel–Tarui theorem is then obtained automatically via the Furst–Saxe–Sipser and Paris–Wilkie translations. As a special case, we obtain a uniform version of Razborov and Smolensky’s representation of AC0[p]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {AC}^{0}[p]$$\end{document} circuits. The paper is partly expository, but is also motivated by the desire to recast Toda’s theorem, the Beigel–Tarui theorem, and their proofs into the language of bounded arithmetic. However, no knowledge of bounded arithmetic is needed. (shrink)

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [44], and show that this analysis can be formalized in the bounded arithmetic system VNC^1 (corresponding to the “NC^1 reasoning”). As a corollary, we prove the assumption made by Jeřábek [28] that a construction of certain bipartite expander graphs can be formalized in VNC^1 . This in turn implies that every proof in Gentzen's sequent calculus LK of a (...) monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlák [9]. (shrink)