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
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 63,417
Through your library

References found in this work BETA

The Foundations of Mathematics.Evert Willem Beth - 1959 - Amsterdam: North-Holland Pub. Co..
On the Scheme of Induction for Bounded Arithmetic Formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (3):261-302.
The Foundations of Mathematics.Charles Parsons & Evert W. Beth - 1961 - Philosophical Review 70 (4):553.
Quantified Propositional Calculi and Fragments of Bounded Arithmetic.Jan Krajíček & Pavel Pudlák - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (1):29-46.

View all 13 references / Add more references

Citations of this work BETA

Incompleteness in the Finite Domain.Pavel Pudlák - 2017 - Bulletin of Symbolic Logic 23 (4):405-441.
A Lower Bound for Intuitionistic Logic.Pavel Hrubeš - 2007 - Annals of Pure and Applied Logic 146 (1):72-90.
Feasibly Constructive Proofs of Succinct Weak Circuit Lower Bounds.Moritz Müller & Ján Pich - 2020 - Annals of Pure and Applied Logic 171 (2):102735.
Proof Complexity of Intuitionistic Implicational Formulas.Emil Jeřábek - 2017 - Annals of Pure and Applied Logic 168 (1):150-190.
On Lengths of Proofs in Non-Classical Logics.Pavel Hrubeš - 2009 - Annals of Pure and Applied Logic 157 (2-3):194-205.

View all 16 citations / Add more citations

Similar books and articles


Added to PP index

Total views
126 ( #84,727 of 2,449,133 )

Recent downloads (6 months)
1 ( #441,480 of 2,449,133 )

How can I increase my downloads?


My notes