## Abstract

The interpolation, method has been one of the main tools for proving lower bounds for propositional proof systems. Loosely speaking, if one can prove that a particular proof system has the feasible interpolation property, then a generic reduction can (usually) be applied to prove lower bounds for the proof system, sometimes assuming a (usually modest) complexity-theoretic assumption. In this paper, we show that this method cannot be used to obtain lower bounds for Frege systems, or even for TC^{0}-Frege systems. More specifically, we show that unless factoring (of Blum integers) is feasible, neither Frege nor TC^{0}-Frege has the feasible interpolation property. In order to carry out our argument, we show how to carry out proofs of many elementary axioms/theorems of arithmetic in polynomial-sized TC^{0}-Frege. As a corollary, we obtain that TC^{0}-Frege, as well as any proof system that polynomially simulates it, is not automatizable (under the assumption that factoring of Blum integers is hard). We also show under the same hardness assumption that the k-provability problem for Frege systems is hard.

Original language | English (US) |
---|---|

Pages (from-to) | 1939-1967 |

Number of pages | 29 |

Journal | SIAM Journal on Computing |

Volume | 29 |

Issue number | 6 |

DOIs | |

State | Published - Apr 2000 |

Externally published | Yes |

## All Science Journal Classification (ASJC) codes

- Computer Science(all)
- Mathematics(all)