The feasible interpolation theorem for semantic derivations from [J. Krajíček, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic 62 457–486] allows to derive from some short semantic derivations of the disjointness of two [Formula: see text] sets [Formula: see text] and [Formula: see text] a small communication protocol computing the Karchmer–Wigderson multi-function [Formula: see text] associated with the sets, and such a protocol further yields a small circuit separating [Formula: see text] from (...) [Formula: see text]. When [Formula: see text] is closed upwards, the protocol computes the monotone Karchmer–Wigderson multi-function [Formula: see text] and the resulting circuit is monotone. Krajíček [Interpolation by a game, Math. Logic Quart. 44 450–458] extended the feasible interpolation theorem to a larger class of semantic derivations using the notion of a real communication complexity. In this paper, we generalize the method to a still larger class of semantic derivations by allowing randomized protocols. We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle, that does correspond to communication protocols for [Formula: see text] making errors. The new randomized feasible interpolation thus shows that a short semantic derivation of the disjointness of [Formula: see text], [Formula: see text] closed upwards, yields a small randomized protocol for [Formula: see text] and hence a small monotone CLO separating the two sets. This research is motivated by the open problem to establish a lower bound for proof system [Formula: see text] operating with clauses formed by linear Boolean functions over [Formula: see text]. The new randomized feasible interpolation applies to this proof system and also to cutting planes CP, to small width resolution over CP of Krajíček [Discretely ordered modules as a first-order extension of the cutting planes proof system, J. Symbolic Logic 63 1582–1596] ) and to random resolution RR of Buss, Kolodziejczyk and Thapen [Fragments of approximate counting, J. Symbolic Logic 79 496–525]. The method does not yield yet lengths-of-proofs lower bounds; for this it is necessary to establish lower bounds for randomized protocols or for monotone CLOs. (shrink)

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)