A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (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)

We study variants of Buss’s theories of bounded arithmetic axiomatized by induction schemes disallowing the use of parameters, and closely related induction inference rules. We put particular emphasis on \ induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems and \ of a new form), results on numbers of instances of the axioms or rules, connections to reflection principles for quantified propositional calculi, and separations between the systems.

For all i ≥ 1, Ti+11 is not ∀Σb2-conservative over Ti1.

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 and G0, (...) in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (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)

The theories Si1 and Ti1 are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. Σbi+1-sentences. The independence (...) results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems. (shrink)