ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F24%3A10487986" target="_blank" >RIV/00216208:11320/24:10487986 - isvavai.cz</a>
Result on the web
<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=Y.rqPZkIUZ" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=Y.rqPZkIUZ</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1017/bsl.2023.40" target="_blank" >10.1017/bsl.2023.40</a>
Alternative languages
Result language
angličtina
Original language name
ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS
Original language description
Cook and Reckhow [5] pointed out that $mathcal {N}mathcal {P} neq comathcal {N}mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows:There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $mathcal {N}mathcal {P}$ sets. We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results), to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from [18] is a good candidate for g. We define a new hardness property of generators, the $bigvee $ -hardness, and show that one specific gadget generator is the $bigvee $ -hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite $mathcal {N}mathcal {P}$ sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite $mathcal {N}mathcal {P}$ sets.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2024
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Bulletin of Symbolic Logic
ISSN
1079-8986
e-ISSN
1943-5894
Volume of the periodical
30
Issue of the periodical within the volume
1
Country of publishing house
US - UNITED STATES
Number of pages
21
Pages from-to
20-40
UT code for WoS article
001195451000001
EID of the result in the Scopus database
2-s2.0-85178007044