We describe a general method how to construct from a propositional proof system P a possibly much stronger proof system iP. The system iP operates with exponentially long P-proofs described “implicitly” by polynomial size circuits.As an example we prove that proof system iEF, implicit EF, corresponds to bounded arithmetic theory V12 and hence, in particular, polynomially simulates the quantified propositional calculus G and the Πb1-consequences of S12 proved with one use of exponentiation. Furthermore, the soundness of iEF is not provable (...) in S12. An iteration of the construction yields a proof system corresponding to T2 + Exp and, in principle, to much stronger theories. (shrink)

We characterize the collapse of Buss' bounded arithmetic in terms of the provable collapse of the polynomial time hierarchy. We include also some general model-theoretical investigations on fragments of bounded arithmetic.

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) withkinferences has an interpolant whose circuit-size is at mostk. 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 ofLKcorresponding to the bounded arithmetic theory(α)(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(α).In the other direction we show that a depth 2 subsystem ofLKdoes not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem ofLKwould yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

A number of theories have been developed to characterize ALogTime (or uniform NC 1, or just NC 1), the class of languages accepted by alternating logtime Turing machines, in the same way that Buss’s theory ${{\bf S}^{1}_{2}}$ characterizes polytime functions. Among these, ALV′ (by Clote) is particularly interesting because it is developed based on Barrington’s theorem that the word problem for the permutation group S 5 is complete for ALogTime. On the other hand, ALV (by Clote), T 0 NC 0 (...) (by Clote and Takeuti) as well as Arai’s theory ${{\bf AID}+\Sigma_0^B{-}{\bf CA}}$ and its two-sorted version VNC 1 (by Cook and Morioka) are based on the circuit characterization of ALogTime. While the last three theories have been known to be equivalent, their relationship to ALV′ has been an open problem. Here we show that ALV′ is indeed equivalent to the other theories. (shrink)

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)

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)

We describe a general method how to construct from a propositional proof system P a possibly much stronger proof system iP. The system iP operates with exponentially long P-proofs described "implicitly" by polynomial size circuits. As an example we prove that proof system iEF, implicit EF, corresponds to bounded arithmetic theory $V_{2}^{1}$ and hence, in particular, polynomially simulates the quantified propositional calculus G and the $\pi_{1}^{b}-consequences$ of $S_{2}^{1}$ proved with one use of exponentiation. Furthermore, the soundness of iEF is not (...) provable in $S_{2}^{1}$ . An iteration of the construction yields a proof system corresponding to $T_{2} + Exp$ and, in principle, to much stronger theories. (shrink)

We characterize the collapse of Buss' bounded arithmetic in terms of the provable collapse of the polynomial time hierarchy. We include also some general model-theoretical investigations on fragments of bounded arithmetic.