Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic

Journal of Symbolic Logic 62 (2):457-486 (1997)
Abstract
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
Options
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
 
Download options
PhilPapers Archive


Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 10,747
External links
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

No references found.

Citations of this work BETA
Pavel Hrubeš (2009). On Lengths of Proofs in Non-Classical Logics. Annals of Pure and Applied Logic 157 (2):194-205.
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.

View all 6 citations

Similar books and articles
Analytics

Monthly downloads

Added to index

2009-01-28

Total downloads

12 ( #126,794 of 1,098,844 )

Recent downloads (6 months)

4 ( #79,596 of 1,098,844 )

How can I increase my downloads?

My notes
Sign in to use this feature


Discussion
Start a new thread
Order:
There  are no threads in this forum
Nothing in this forum yet.