Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
A. J. Wilkie & J. B. Paris (1987). On the Scheme of Induction for Bounded Arithmetic Formulas. Annals of Pure and Applied Logic 35 (3):261-302.
Jan Krajíček & Pavel Pudlák (1990). Quantified Propositional Calculi and Fragments of Bounded Arithmetic. Mathematical Logic Quarterly 36 (1):29-46.
Jan Krajíček & Pavel Pudlák (1990). Quantified Propositional Calculi and Fragments of Bounded Arithmetic. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (1):29-46.
Daniele Mundici (1984). Tautologies with a Unique Craig Interpolant, Uniform Vs. Nonuniform Complexity. Annals of Pure and Applied Logic 27 (3):265-273.
Citations of this work BETA
Pavel Hrubeš (2007). A Lower Bound for Intuitionistic Logic. Annals of Pure and Applied Logic 146 (1):72-90.
Jan Krajicek (2001). Tautologies From Pseudo-Random Generators. Bulletin of Symbolic Logic 7 (2):197-212.
Samuel R. Buss & Pavel Pudlák (2001). On the Computational Content of Intuitionistic Propositional Proofs. Annals of Pure and Applied Logic 109 (1-2):49-64.
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.
Pavel Hrubeš (2009). On Lengths of Proofs in Non-Classical Logics. Annals of Pure and Applied Logic 157 (2):194-205.
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 downloads19 ( #206,668 of 1,934,839 )
Recent downloads (6 months)1 ( #434,687 of 1,934,839 )
How can I increase my downloads?