EN
We study diagonalization in the context of implicit proofs of [10]. We prove that at least one of the following three conjectures is true:
∙ There is a function f: {0,1}* → {0,1} computable in 𝓔 that has circuit complexity $2^{Ω(n)}$.
∙ 𝓝 𝓟 ≠ co 𝓝 𝓟.
∙ There is no p-optimal propositional proof system.
We note that a variant of the statement (either 𝓝 𝓟 ≠ co 𝓝 𝓟 or 𝓝 𝓔 ∩ co 𝓝 𝓔 contains a function $2^{Ω(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.