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

*(English)*Zbl 0891.03029This article is a supplement, so to say, to the author’s monograph: Bounded arithmetic, propositional logic, and complexity theory (1995; Zbl 0835.03025), and the author provides the following 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 (\alpha)\),

(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 A. A. Razborov [Izv. Ross. Akad. Nauk, Ser. Mat. 59, No. 1, 201-224 (1995; Zbl 0838.03045)] 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.”

What is not said in the above abstract is that this paper also serves as a guide to the literature. It carries 46 references, and the author comments on them at pertinent points throughout the text.

“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,

(b) for the cutting planes proof system with coefficients written in unary.

(3) An alternative proof of the independence result of A. A. Razborov [Izv. Ross. Akad. Nauk, Ser. Mat. 59, No. 1, 201-224 (1995; Zbl 0838.03045)] 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.”

What is not said in the above abstract is that this paper also serves as a guide to the literature. It carries 46 references, and the author comments on them at pertinent points throughout the text.

Reviewer: M.Yasuhara (Princeton)

##### MSC:

03F20 | Complexity of proofs |

03F30 | First-order arithmetic and fragments |

03B05 | Classical propositional logic |

03D15 | Complexity of computation (including implicit computational complexity) |

68Q15 | Complexity classes (hierarchies, relations among complexity classes, etc.) |

##### Keywords:

Craig interpolation theorem; interpolant; circuit-size; communication complexity; proof systems; bounded arithmetic; exponential lower bounds; feasible monotone interpolation theorem; weak pigeonhole principle
Full Text:
DOI

##### References:

[1] | Prepositional proof systems, the consistency of first order theories and the complexity of computations 54 pp 1063– (1989) |

[2] | Computer Science Logic pp 193– (1989) · Zbl 0685.03002 |

[3] | Bounded arithmetic, prepositional logic and complexity theory (1995) |

[4] | Lower bounds to the size of constant-depth prepositional proofs 59 pp 73– (1994) |

[5] | Logic from Computer Science, Proceedings of a workshop held November 13–17, 1989, in Berkeley, Mathematical Sciences Research Institute Publication pp 287– (1992) |

[6] | Annals of Pure and Applied Logic 48 pp 261– (1989) |

[7] | Proceedings of the 20th Annual ACM Symposium on Theory of Computing pp 539– (1988) |

[8] | DOI: 10.1016/0304-3975(85)90144-6 · Zbl 0586.03010 |

[9] | Arithmetic, Proof Theory and Computational Complexity pp 364– (1993) |

[10] | Proceedings of Logic Colloquium 1983 pp 175– (1984) |

[11] | Proof theory (1975) · Zbl 0354.02027 |

[12] | DOI: 10.1016/0001-8708(76)90167-5 · Zbl 0355.02010 |

[13] | Proceedings of the 26th Annual ACM Symposium on Theory of Computing pp 204– (1994) |

[14] | Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory 22 pp 269– (1957) · Zbl 0079.24502 |

[15] | Izvestiya of the R. A. N. 59 pp 201– (1995) |

[16] | Linear reasoning: A new form of the Herbrand-Gentzen theorem 22 pp 250– (1957) · Zbl 0081.24402 |

[17] | DOI: 10.1007/978-1-4612-2566-9_12 |

[18] | DOI: 10.1016/0166-218X(87)90039-4 · Zbl 0625.90056 |

[19] | Arithmetic, Proof Theory and Computational Complexity pp 247– (1993) |

[20] | The relative efficiency of prepositional proof systems 44 pp 36– (1979) |

[21] | Proceedings of the 7th Annual ACM Symposium on Theory of Computing pp 83– (1975) |

[22] | Soviet Mathem. Doklady 31 pp 354– (1985) |

[23] | DOI: 10.1137/0204018 · Zbl 0316.68031 |

[24] | DOI: 10.1016/0304-3975(88)90072-2 · Zbl 0709.03006 |

[25] | Bounded arithmetic (1986) |

[26] | Provability of the pigeonhole principle and the existence of infinitely many primes 53 pp 1235– (1988) · Zbl 0688.03042 |

[27] | DOI: 10.1016/0168-0072(87)90066-2 · Zbl 0647.03046 |

[28] | The foundations of mathematics (1959) |

[29] | Methods in Mathematical Logic pp 317– (1985) |

[30] | Doklady ANSSSR 282 pp 1033– (1985) |

[31] | Existence and feasibility in arithmetic 36 pp 494– (1971) |

[32] | DOI: 10.1007/BF02579196 · Zbl 0631.68041 |

[33] | Computational complexity (1994) · Zbl 0833.68049 |

[34] | DOI: 10.1016/0168-0072(84)90029-0 · Zbl 0594.03022 |

[35] | Proceedings of Logic Colloquium 1982 pp 345– (1984) |

[36] | DOI: 10.1007/BF02023010 · Zbl 0511.03004 |

[37] | Pseudo-randomness and applications (1993) |

[38] | Technical report nb. 3 (1961) |

[39] | DOI: 10.1007/BF01531024 · Zbl 0865.03045 |

[40] | DOI: 10.1007/978-1-4612-3466-1_15 |

[41] | Proceedings of the meeting Logic and Computational Complexity (1995) |

[42] | DOI: 10.1002/malq.19900360106 · Zbl 0696.03031 |

[43] | DOI: 10.1007/978-1-4612-2566-9_10 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.