Diagonalization in proof complexity

Jan Krajíček¹

¹ Mathematical Institute Academy of Sciences Žitná 25 CZ 115 67 Praha 1, Czech Republic

Fundamenta Mathematicae, Tome 182 (2004) no. 2, pp. 181-192.

Résumé

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.

Détail

DOI : 10.4064/fm182-2-7

Keywords: study diagonalization context implicit proofs prove least following three conjectures bullet there function * rightarrow computable cal has circuit complexity mit omega bullet cal cal neq mathop cal cal bullet there p optimal propositional proof system note variant statement either cal cal neq mathop cal cal cal cal cap mathop cal cal contains function mit omega hard average seems have bearing existence proof complexity generators particular prove minor variant recent conjecture razborov conjecture stating conditional lower bounds extended frege proof system nbsp actually unconditional lower bounds would follow nbsp