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

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 ([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)
DOI 10.2307/2275541
 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: 16,667
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.

Add more references

Citations of this work BETA
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.
Samuel R. Buss (2012). Towards–Via Proof Complexity and Search. Annals of Pure and Applied Logic 163 (7):906-917.

View all 7 citations / Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

15 ( #175,565 of 1,726,994 )

Recent downloads (6 months)

3 ( #231,303 of 1,726,994 )

How can I increase my downloads?

My notes
Sign in to use this feature

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