Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 62 (2):457-486 (1997)
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 () (b) for the cutting planes proof system with coefficients written in unary (). (3) An alternative proof of the independence result of  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
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
References found in this work BETA
No references found.
Citations of this work BETA
Arnold Beckmann & Samuel R. Buss (2005). Separation Results for the Size of Constant-Depth Propositional Proofs. Annals of Pure and Applied Logic 136 (1-2):30-55.
Samuel R. Buss (2012). Towards–Via Proof Complexity and Search. Annals of Pure and Applied Logic 163 (7):906-917.
Pavel Hrubeš (2007). A Lower Bound for Intuitionistic Logic. Annals of Pure and Applied Logic 146 (1):72-90.
Pavel Hrubeš (2009). On Lengths of Proofs in Non-Classical Logics. Annals of Pure and Applied Logic 157 (2):194-205.
Ján Pich (2011). Nisan-Wigderson Generators in Proof Systems with Forms of Interpolation. Mathematical Logic Quarterly 57 (4):379-383.
Similar books and articles
Samuel R. Buss (1994). On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedup for Arithmetics. Journal of Symbolic Logic 59 (3):737-756.
Samuel R. Buss (1987). Polynomial Size Proofs of the Propositional Pigeonhole Principle. Journal of Symbolic Logic 52 (4):916-927.
Pavel Hrubeš (2007). Lower Bounds for Modal Logics. Journal of Symbolic Logic 72 (3):941 - 958.
Hiroakira Ono (1986). Craig's Interpolation Theorem for the Intuitionistic Logic and its Extensions—a Semantical Approach. Studia Logica 45 (1):19 - 33.
Jan Krajiček (1994). Lower Bounds to the Size of Constant-Depth Propositional Proofs. Journal of Symbolic Logic 59 (1):73-86.
Maria Luisa Bonet & Samuel R. Buss (1993). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (2):688-709.
Pavel Pudlák (1997). Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62 (3):981-998.
Maria Bonet, Toniann Pitassi & Ran Raz (1997). Lower Bounds for Cutting Planes Proofs with Small Coefficients. Journal of Symbolic Logic 62 (3):708-728.
Jan Krajíček (1995). Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press.
Jan Krajíček (1998). Discretely Ordered Modules as a First-Order Extension of the Cutting Planes Proof System. Journal of Symbolic Logic 63 (4):1582-1596.
Added to index2009-01-28
Total downloads8 ( #138,555 of 1,088,389 )
Recent downloads (6 months)0
How can I increase my downloads?