Search

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 (of Blum integers) 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-sized TC0-Frege. As a corollary, we obtain that TC0-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.

The serial transitive closure problem is the problem of, given a directed graph $G$ and a list of edges, called closure edges, which are in the transitive closure of the graph, to generate all the closure edges from edges in $G$. A nearly linear upper bound is given on the number of steps in optimal solutions to the serial transitive closure problem for the case of graphs which are trees. "Nearly linear" means $O(n\cdot \alpha(n))$ where $\alpha$ is the inverse Ackermann function. This upper bound is optimal to within a constant factor.