Diagonalization in proof complexity

Jan Krajíček

Fundamenta Mathematicae (2004)

  • Volume: 182, Issue: 2, page 181-192
  • ISSN: 0016-2736

Abstract

top
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.

How to cite

top

Jan Krajíček. "Diagonalization in proof complexity." Fundamenta Mathematicae 182.2 (2004): 181-192. <http://eudml.org/doc/286451>.

@article{JanKrajíček2004,
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: ∙ 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.},
author = {Jan Krajíček},
journal = {Fundamenta Mathematicae},
keywords = {propositional proof system},
language = {eng},
number = {2},
pages = {181-192},
title = {Diagonalization in proof complexity},
url = {http://eudml.org/doc/286451},
volume = {182},
year = {2004},
}

TY - JOUR
AU - Jan Krajíček
TI - Diagonalization in proof complexity
JO - Fundamenta Mathematicae
PY - 2004
VL - 182
IS - 2
SP - 181
EP - 192
AB - 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.
LA - eng
KW - propositional proof system
UR - http://eudml.org/doc/286451
ER -

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.