If no optimal propositional proof system exists, we (and independently Pudl\'ak) prove that ruling out length $t$ proofs of any unprovable sentence is hard. This mapping from unprovable to hard-to-prove sentences powerfully translates facts about noncomputability into complexity theory. For instance, because proving string $x$ is Kolmogorov random ($x{\in}R$) is typically impossible, it is typically hard to prove "no length $t$ proof shows $x{\in}R$", or tautologies encoding this. Therefore, a proof system with one family of hard tautologies has these densely in an enumeration of families. The assumption also implies that a natural language is $\textbf{NP}$-intermediate: with $R$ redefined to have a sparse complement, the complement of the language $\{\langle x,1^t\rangle|$ no length $t$ proof exists of $x{\in}R\}$ is also sparse. Efficiently ruling out length $t$ proofs of $x{\in}R$ might violate the constraint on using the fact of $x{\in}R$'s unprovability. We conjecture: any computable predicate on $R$ that might be used in if-then statements (or case-based proofs) does no better than branching at random, because $R$ appears random by any effective test. This constraint could also inhibit the usefulness in circuits and propositional proofs of NOT gates and cancellation -- needed to encode if-then statements. If $R$ defeats if-then logic, exhaustive search is necessary.
翻译:如果不存在最优命题证明系统,我们(以及Pudl\'{a}k)证明,排除任何不可证明句子的长度为$t$的证明是困难的。从不可计算性到复杂性理论的这种映射将非计算性事实强有力地转化为复杂性理论。例如,因为证明字符串$x$为 Kolmogorov 随机序列($x{\in}R$)通常是不可能的,所以证明“长度为$t$的证明没有展示$x{\in}R$”或者编码这个的tautologies通常是困难的。因此,有一个具有一个困难tautologies族的证明系统在这个族的枚举中有着密集的存在。这个假设还意味着自然语言是$\textbf{NP}$-intermediate:当将$R$重新定义为具有稀疏补集时,$x{\in}R$不存在长度为$t$的证明的集合的补集也是稀疏的。有效地排除$x{\in}R$的长度为$t$的证明可能违反$x{\in}R$不可证明的事实的限制。我们猜想:任何可能被用于if-then语句(或基于案例的证明)中的$R$的计算谓词执行的效果都不会比随机分支更好,因为通过任何有效性检验,$R$看起来都是随机的。这个限制也可能阻碍NOT门和消除的电路和命题证明的有用性-这些都是用于编码if-then语句。如果$R$击败了if-then逻辑,穷尽搜索是必要的。