No feasible interpolation for TC0-Frege proofs

Maria Luisa Bonet, Toniann Pitassi, Ran Raz

Research output: Contribution to journalConference articlepeer-review

20 Scopus citations


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 TC0-Frege systems. More specifically, we show that unless factoring is feasible, neither Frege nor TC0-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-size TC0-Frege. In particular, we show how to carry out the proof for the Chinese Remainder Theorem, which may be of independent interest. As a corollary, we obtain that TC0-Frege as well as any proof system that polynomially simulates it, is not automatizable (under a hardness assumption).

Original languageEnglish (US)
Pages (from-to)254-263
Number of pages10
JournalAnnual Symposium on Foundations of Computer Science - Proceedings
StatePublished - 1997
Externally publishedYes
EventProceedings of the 1997 38th IEEE Annual Symposium on Foundations of Computer Science - Miami Beach, FL, USA
Duration: Oct 20 1997Oct 22 1997

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture


Dive into the research topics of 'No feasible interpolation for TC0-Frege proofs'. Together they form a unique fingerprint.

Cite this