A proof complexity conjecture and the Incompleteness theorem

1. Problem Statement

The paper addresses a central open problem in proof complexity: the existence of a proof complexity generator.

• The Conjecture: Does there exist a polynomial-time (p-time) function $g: \{0, 1\}^* \to \{0, 1\}^*$ that stretches every input by exactly one bit (i.e., $|g(u)| = |u| + 1$) such that its range, $\text{Rng}(g)$, intersects all infinite NP sets?
• Significance: If such a generator exists, it implies that no propositional proof system can efficiently prove the non-membership of strings in the range of $g$. This would have profound implications for the separation of complexity classes (specifically implying $\text{NP} \neq \text{coNP}$) and the non-existence of optimal proof search algorithms.
• The Gap: While the conjecture is widely believed, proving the existence of such a function for all NP sets remains an open problem. Krajíček investigates this by constructing a function based on logical provability and analyzing its properties.

2. Methodology

The author employs a two-pronged approach, moving from first-order logic to propositional logic:

A. First-Order Construction (Theoretical Foundation)

1. Framework: The construction is based on a sound, p-time, first-order theory $T$ (specifically $S^1_2$ of Buss) capable of formalizing the syntax of first-order logic.
2. Function Definition ($g_T$):
   • Input: A binary string $u$ of length $n$.
   • Step 1: Identify a short formula $\Phi$ (length $\le \log n$) embedded as a prefix of $u$.
   • Step 2: Iterate through all binary strings $w$ of length $c+1$ (where $c = |\Phi|$). For each $w$, search for a $T$-proof of size $\le \log n$ for the sentence:
     $$\exists y \forall x > y (\Phi(x) \to \neg(w \subseteq_e x))$$
     This sentence essentially asserts that $w$ is not a prefix of any sufficiently long element in the set defined by $\Phi$.
   • Step 3: If a proof is found for all $w$, output $0^{n+1}$. Otherwise, output $w_0 u_0$, where $w_0$ is the first $w$ for which no proof exists, and $u = \Phi u_0$.
3. Logical Analysis: The author analyzes the properties of $g_T$ assuming $T$ is sound and complete.

B. Propositional Translation (Complexity Reduction)

To connect the first-order result to computational complexity classes, the author translates the logic into propositional logic:

1. Translation: Uses the canonical propositional translation of $\Sigma^b_1$ formulas. The sentence $\Phi_w$ (which is $\Pi^b_1$) is translated into a propositional formula $\varphi_{n,w}$.
2. Assumptions: The proof assumes the negation of two major complexity statements:
   • There exists a p-optimal propositional proof system (Statement 1).
   • $\text{E} \subseteq \text{P/poly}$ (Statement 2).
3. Circuit Simulation: Under the assumption $\text{E} \subseteq \text{P/poly}$, the function computing proofs in the optimal system can be represented by small circuits. The author constructs a new function $h$ that searches for proofs not by running a general algorithm, but by iterating through truth tables of small circuits (simulating the proof search).

3. Key Contributions and Results

Result 1: A New Proof of Gödel's First Incompleteness Theorem

• Theorem 2.2 & Corollary 2.3: The paper demonstrates that if $T$ is a sound, p-time theory extending $S^1_2$, it cannot be complete.
• Mechanism: The function $g_T$ is constructed such that if $T$ were complete, its range would intersect every infinite definable set. However, the complement of the range, $\{0, 1\}^* \setminus \text{Rng}(g_T)$, is itself an infinite definable set. If $T$ were complete, it would have to prove the non-existence of elements in the complement that actually exist, leading to a contradiction.
• Significance: This provides a proof-theoretic derivation of Gödel's theorem using the properties of proof complexity generators, rather than self-reference (diagonalization).

Result 2: The Trichotomy Theorem (Main Theorem)

The paper establishes that at least one of the following three statements must be true (Theorem 3.1):

1. No p-optimal propositional proof system exists: This is equivalent to saying there is no time-optimal algorithm for propositional proof search.
2. $\text{E} \not\subseteq \text{P/poly}$: The class of problems solvable in exponential time is not contained in non-uniform polynomial-size circuits.
3. Existence of a Hard Generator: There exists a function $h$ such that:
   • It stretches inputs by one bit ($|h(u)| = |u| + 1$).
   • It is computable in sub-exponential time ($2^{O((\log n)^{\log \log n})}$).
   • Its range intersects all infinite NP sets.

4. Technical Details of the Propositional Construction

• Function $h_P$: The paper constructs $h_P$ by simulating the search for proofs in a hypothetical p-optimal system.
• Complexity Analysis:
  • The search space involves iterating through all possible strings $w$ and checking if a proof exists.
  • By assuming $\text{E} \subseteq \text{P/poly}$, the proof search is reduced to checking truth tables of circuits with size roughly $(\log n)^{\log \log n}$.
  • The total time complexity is dominated by the enumeration of these circuits, resulting in the sub-exponential bound $2^{O((\log n)^{\log \log n})}$.
• Intersection Property: The construction ensures that for any infinite NP set defined by a $\Sigma^b_1$ formula, the function $h_P$ will eventually output a string in that set (unless a proof of non-membership is found, which the construction avoids by design if the set is infinite).

5. Significance and Open Problems

• Bridging Logic and Complexity: The paper successfully bridges the gap between logical incompleteness and computational hardness. It shows that the difficulty of proving the non-membership of strings in the range of a stretching function is intrinsically linked to the existence of optimal proof systems and circuit lower bounds.
• Refining the Conjecture: While the paper does not definitively prove the existence of a generator hard for all NP sets (which would require proving $\text{NP} \neq \text{coNP}$), it narrows the landscape. It proves that if we assume standard complexity conjectures (like $\text{E} \not\subseteq \text{P/poly}$ or the non-existence of optimal proof systems), the generator exists.
• Open Problem 2.4: The author explicitly leaves open whether the specific function $g_T$ (or a variant) satisfies the conjecture for all NP sets. The affirmative answer would imply $\text{NP} \neq \text{coNP}$.
• Implications for Proof Search: The result suggests that if optimal proof search algorithms do exist, then either $\text{E} \not\subseteq \text{P/poly}$ is false (unlikely) or a very efficient generator exists that intersects all NP sets.

In summary, Krajíček provides a rigorous framework linking the incompleteness of formal theories to the hardness of proof complexity generators, offering a conditional proof that such generators exist under standard complexity assumptions, and providing a novel proof of Gödel's theorem based on these concepts.