On the existence of strong proof complexity generators

TL;DR

The paper investigates whether a uniform p-time generator $g$ with stretch $m(n)=n+1$ can intersect every infinite ${ m NP}$ set, i.e., whether there exists a generator hard for all proof systems. It develops notions of feasible disjunction property and $igvee$-hardness, and constructs gadget generators (notably ${ m Gad}_{sq}$) that are $igvee$-hard for broad proof systems, connecting lower-bound hardness to structured combinatorial gadgets. The work analyzes stretch limits via time-bounded Kolmogorov complexity ($K^t$ and $Kt$) and examines witnessing of the dual weak pigeonhole principle in bounded arithmetic, showing conditional results under Hypothesis (H) and highlighting barriers posed by extreme-stretch strings. It also introduces the concept of feasibly infinite ${ m NP}$ sets and proves a relative version of the conjecture for these sets, linking to model-theoretic and arithmetic perspectives. Overall, the paper maps a landscape of conditional and structural results toward a strong generator conjecture, identifying concrete avenues (gadgets, fdp, proof-search variants) and fundamental obstacles for establishing provable hardness for all proof systems.

Abstract

Cook and Reckhow 1979 pointed out that NP is not closed under complementation iff there is no propositional proof system that admits polynomial size proofs of all tautologies. Theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus at a conjecture from K.2004 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 exist a p-time function $g$ stretching each input by one bit such that its range intersects all infinite NP 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 K.2009 is a good candidate for $g$. We define a new hardness property of generators, the $\bigvee$-hardness, and shows that one specific gadget generator is the $\bigvee$-hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite NP sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite NP sets.

Theorems & Definitions (14)

• Conjecture 1.1: Kra-dual
• Theorem 2.1: Kra-small
• Theorem 2.2
• Definition 3.1
• Lemma 3.2
• Lemma 3.3
• Theorem 4.1: ess.Kra-generator
• Lemma 4.2
• Theorem 5.1: Allender All
• Theorem 5.3