Abstract:
We study the diagonalization in the context of proof complexity. We prove that at least one of the following three conjectures is true: 1. There is a boolean function computable in E that has circuit complexity $2^{\Omega(n)}$. 2. NP is not closed under the complement. 3. There is no p-optimal propositional proof system. We note that a variant of the statement 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 is true (stating conditional lower bounds for the Extended Frege proof system EF) then actually unconditional lower bounds would follow for EF.