论文标题
证明重言和定理的平均硬度硬度
Average-Case Hardness of Proving Tautologies and Theorems
论文作者
论文摘要
我们合并了两个广泛认为的关于重言式的猜想 - 不存在最佳证明系统，并且大多数要求在任何系统中都需要超级单位尺寸的证明 - 将所有可允许的$ \ textbf {conp} $满足的$ p $ - 异晶不变条件 - - 完整的语言或无。条件是：对于接受该语言的任何图灵机（TM）$ m $，$ \ textbf {p} $ - 统一输入的家庭需要$ m $乘$ m $（相当于第一个猜想），并且在投入自己的投入量的枚举中以正密度出现（暗示第二个）。在这种情况下，对于分发，对艰难家庭施加不可忽略的重量的分配，这种语言平均不容易（以$ \ textbf {avgp} $）。 证明重言和定理的硬度可能是相关的。由算术句子编码“字符串$ x $是kolmogorov随机”的动机是真实但无法证明的，在有限的公理化理论$ \ mathcal $ \ mathcal {t} $（calude and j { ^ ud} rgensen）中，我们想到任何需要命题的命题系统尺寸的dicrolects supterialnomolomial spults septers supteriquely supters septers dicroper supterial supters septs did d d d d d d d d d d dive $ \ textbf {p} $ - 编码的重言式统一家庭“没有$ \ mathcal {t} $ size y size $ \ leq t $的证明，显示字符串$ x $是kolmogorov随机的”。这意味着上述条件。 该猜想表明没有最佳的证明系统，因为不可确定的理论有助于证明重言术，并且随着添加公理的添加而更有效地做到这一点，并且构建硬式训练似乎很困难，因为不可能构建kolmogorov随机弦。类似的猜想是，计算盲点是不可误性的表现会解决其他开放问题。
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{ü}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.
