Publishing house / Journals and Serials / Fundamenta Mathematicae / All issues

Abstract

We study diagonalization in the context of implicit proofs of [10]. We prove that at least one of the following three conjectures is true:

$\bullet$ There is a function $f : \{0, 1\}^{*} \rightarrow \{0,1\}$ computable in ${\cal E}$ that has circuit complexity $2^{{\mit\Omega}(n)}$.

$\bullet$ ${\cal N}{\cal P} \neq \mathop{\rm co} {\cal N}{\cal P}$.

$\bullet$ There is no $p$-optimal propositional proof system.

We note that a variant of the statement (either ${\cal N}{\cal P} \neq \mathop{\rm co}{\cal N}{\cal P}$ or ${\cal N}{\cal E}\cap \mathop{\rm co}{\cal N}{\cal E}$ contains a function $2^{{\mit\Omega}(n)}$ hard on average) seems to have a bearing on the existence of good proof complexity generators. In particular, we prove that if a minor variant of a recent conjecture of Razborov [17, Conjecture 2] is true (stating conditional lower bounds for the Extended Frege proof system EF) then actually unconditional lower bounds would follow for EF.