Average-Case Hardness of Proving Tautologies and Theorems

TL;DR

This paper links the average-case hardness of tautologies and the nonexistence of optimal proof systems to conjectures about superpolynomial proof sizes, Kolmogorov randomness, and noncomputability, proposing a unified invariant condition.

Contribution

It introduces a $p$-isomorphism-invariant condition connecting proof complexity conjectures with properties of paddable coNP-complete languages and proposes a new conjecture relating proof size and Kolmogorov randomness.

Findings

Consolidates two major conjectures into a single invariant condition.

Proposes a new conjecture linking proof complexity with Kolmogorov randomness.

Suggests that the hardness of proving tautologies is related to noncomputability and randomness.

Abstract

We consolidate two widely believed conjectures about tautologies -- no optimal proof system exists, and most require superpolynomial size proofs in any system -- into a $p$-isomorphism-invariant condition satisfied by all paddable $\textbf{coNP}$-complete languages or none. The condition is: for any Turing machine (TM) $M$ accepting the language, $\textbf{P}$-uniform input families requiring superpolynomial time by $M$ exist (equivalent to the first conjecture) and appear with positive upper density in an enumeration of input families (implies the second). In that case, no such language is easy on average (in $\textbf{AvgP}$) for a distribution applying non-negligible weight to the hard families. The hardness of proving tautologies and theorems is likely related. Motivated by the fact that arithmetic sentences encoding "string $x$ is Kolmogorov random" are true but unprovable with positive density in a finitely axiomatized theory $\mathcal{T}$ (Calude and J{\"u}rgensen), we conjecture that any propositional proof system requires superpolynomial size proofs for a dense set of $\textbf{P}$-uniform families of tautologies encoding "there is no $\mathcal{T}$ proof of size $\leq t$ showing that string $x$ is Kolmogorov random". This implies the above condition. The conjecture suggests that there is no optimal proof system because undecidable theories help prove tautologies and do so more efficiently as axioms are added, and that constructing hard tautologies seems difficult because it is impossible to construct Kolmogorov random strings. Similar conjectures that computational blind spots are manifestations of noncomputability would resolve other open problems.