Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP?

Such an oracle will need to satisfy the following condition about DDH:

Is there an oracle such that in the world relativized to it, DDH$_n$ has subexponential $2^{O(n^{1 \over d})}$ size circuits but does not have polynomial ones?


We were talking with Yuval about the possibility of reducing FIP for Frege to FIP for bd-Frege. Up to cryptographic assumption about hardness of DDH (Decisional Diffie–Hellman problem) neither satisfies FIP. The hardness condition on DDH is (exponentially) stronger in the case of bd-Frege [BPR'00,BDGMP'04]. We wanted to see if we can weaken the hardness condition on DDH in the bd-Frege case to the same condition in the Frege case.

Note that the FIP for Frege would trivially imply the FIP for bounded-depth Frege since the former p-simulates the later. There are sub-exponential simulation results in the other direction [FPS'11], but it is not clear if one can obtain FIP for Frege implies FIP for bd-Frege.

On the other hand, for FIP it seems that we need to find the interpolant for cut rules in the proof which is close to finding a satisfying witness for a formula. The formula is of bounded depth in the case of bd-Frege, but the problem of finding a satisfying assignment is not easier than the general case of an arbitrary formula (the Frege case), both are $\mathsf{NP\text{-}complete}$.


One of the main problems in proof complexity is showing superpolynomial lowerbounds for propositional proof systems. If every propositional proof system has a family of formulas with superpolynomial proof size lowerbound, then it follows $\mathsf{NP} \neq \mathsf{coNP}$. So proving lowerbounds for propositional proof systems is similar to proving lowerbounds for circuit families (with the ultimate goal of showing a (general circuit) superpolynomial size lowerbound for some explicit function and separating $\mathsf{NP}$ from $\mathsf{P}/\mathsf{poly}$).

There is a nice correspondence between many propositional proof systems and circuit complexity classes: restrict the lines in the proof to circuits from the corresponding class.

But proving lowerbounds for propositional proof systems seems to be even more difficult than proving circuit lowerbounds, for example we still don't have a lowerbound for the propositional proof system with $AC^0[ 2 ]$ lines where as subexponential size lowerbound are known for $AC^0[ 2 ]$ circuits computing $\mod 3$. Therefore transferring the results from circuit complexity to proof complexity is not straightforward.

One of the few methods for proving proof complexity lowerbounds is showing that the proof system has FIP, and then use it to extract a reasonably small size circuit from the propositional proof of a formula coming from circuit complexity such that we know (or conjecture) the function computed by the interpolant is hard.

FIP for a propositional proof system $P$ means that if $P$ proves a disjunction $\varphi(\vec{x},\vec{y}) \lor \psi(\vec{x},\vec{z})$ then there is a small circuit that given values for $\vec{x}$, tell us which disjunct is true (think of each disjunct as a $\mathsf{coNP}$ set in input $\vec{x}$, and their union covers all possible values of $\vec{x}$, or equivalently the task is separating two provably disjoint $\mathsf{NP}$ sets using polynomial size circuits).

But unfortunately this doesn't work for even relatively weak systems like bd-Frege because up to cryptographic hardness assumptions mentioned above, these systems do not have FIP (they can prove cryptographic results such that an interpolant for the proof would break the cryptographic primitive).


  1. Y. Filmus, T. Pitassi, R. Santhanam, Exponential lower bounds for AC0-Frege imply polynomial Frege lower bounds, ICALP 2011
  2. M.L. Bonet, T. Pitassi, and R. Raz, On interpolation and automatization for Frege systems, SIAM Journal on Computing, 2000.
  3. M.L. Bonet, C. Domingo, R. Gavalda, A. Maciel, and T. Pitassi, Non-automatizability of bounded-depth Frege proofs, Computational Complexity, 2004.

Cross posted on MO


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.