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ák）证明：对于任何不可证明的语句，排除其长度为$t$的证明是困难的。这种从不可证明语句到难证明语句的映射有效地将不可计算性的事实转化为复杂性理论中的结果。例如，由于证明字符串$x$是Kolmogorov随机的（$x{\in}R$）通常是不可能的，那么证明“不存在长度为$t$的证明表明$x{\in}R$”或编码此事实的重言式通常是困难的。因此，一个包含一族困难重言式的证明系统会在枚举的族中密集地出现。该假设还蕴含一种自然语言是$\textbf{NP}$-中间语言：重新定义$R$使其补集稀疏后，语言$\{\langle x,1^t\rangle|$不存在长度为$t$的证明表明$x{\in}R\}$的补集也是稀疏的。高效排除$x{\in}R$的长度为$t$的证明可能违反利用$x{\in}R$不可证明性这一事实的约束。我们猜想：任何可能用于条件语句（或基于情形的证明）中关于$R$的可计算谓词，其效果不会优于随机分支，因为$R$在任何有效检验下都表现为随机的。这种约束还可能抑制NOT门和消去法在电路和命题证明中的有用性——这些是编码条件语句所必需的。如果$R$战胜了条件逻辑，穷举搜索就是必要的。