Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic
Krajicek, Jan
J. Symbolic Logic, Tome 62 (1997) no. 1, p. 457-486 / Harvested from Project Euclid
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(\alpha)$ (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(\alpha)$. 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.
Publié le : 1997-06-14
Classification:  03F20,  03F30,  68Q25
@article{1183745237,
     author = {Krajicek, Jan},
     title = {Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic},
     journal = {J. Symbolic Logic},
     volume = {62},
     number = {1},
     year = {1997},
     pages = { 457-486},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745237}
}
Krajicek, Jan. Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. J. Symbolic Logic, Tome 62 (1997) no. 1, pp.  457-486. http://gdmltest.u-ga.fr/item/1183745237/