排除不可证句子的短证明是困难的

如果不存在最优命题证明系统，我们（以及独立的Pudlák）证明了排除任意不可证句子的长度$t$证明是困难的。这种从不可计算到难证句子的映射有力地将非可计算性事实转化为复杂性理论。例如，因为证明字符串$x$是Kolmogorov随机的（$x{\in}R$）通常是不可能的，通常很难证明“没有长度$t$证明表明$x{\in}R$”，或编码此事实的重言式。因此，具有一族困难重言式的证明系统在这些族的枚举中稠密地拥有这些。该假设还蕴含一种自然语言是$\textbf{NP}$中间的：将$R$重定义为具有稀疏补集后，语言$\{\langle x,1^t\rangle|$ 不存在$x{\in}R$的长度$t$证明$\}$的补集也是稀疏的。高效排除$x{\in}R$的长度$t$证明可能违反关于使用$x{\in}R$不可证性事实的约束。我们猜想：在if-then语句（或基于情形的证明）中可能使用的任何关于$R$的可计算谓词都不比随机分支更好，因为$R$在任何有效检验下都表现为随机。该约束也可能抑制NOT门和消去（编码if-then语句所需）在电路和命题证明中的有用性。如果$R$击败if-then逻辑，则穷举搜索是必要的。