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 . ∙ ≠ co . ∙ There is no p-optimal propositional proof system. We note that a variant of the statement (either ≠ co or ∩ co contains a function 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.
@article{bwmeta1.element.bwnjournal-article-doi-10_4064-fm182-2-7,
author = {Jan Kraj\'\i \v cek},
title = {Diagonalization in proof complexity},
journal = {Fundamenta Mathematicae},
volume = {184},
year = {2004},
pages = {181-192},
zbl = {1068.03049},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.bwnjournal-article-doi-10_4064-fm182-2-7}
}
Jan Krajíček. Diagonalization in proof complexity. Fundamenta Mathematicae, Tome 184 (2004) pp. 181-192. http://gdmltest.u-ga.fr/item/bwmeta1.element.bwnjournal-article-doi-10_4064-fm182-2-7/