Given a sound first-order p-time theory $T$ capable of formalizing syntax of first-order logic we define a p-time function $g_T$ that stretches all inputs by one bit and we use its properties to show that $T$ must be incomplete. We leave it as an open problem whether for some $T$ the range of $g_T$ intersects all infinite NP sets (i.e. whether it is a proof complexity generator hard for all proof systems). A propositional version of the construction shows that at least one of the following three statements is true: - there is no p-optimal propositional proof system (this is equivalent to the non-existence of a time-optimal propositional proof search algorithm), - $E \not\subseteq P/poly$, - there exists function $h$ that stretches all inputs by one bit, is computable in sub-exponential time and its range $Rng(h)$ intersects all infinite NP sets.
翻译:在给定一个能够形式化一阶逻辑句法的声音一阶p-时间理论$T$的情况下,我们定义了一个p-时间函数$g_T$,它通过一位拉长所有输入,并使用其属性来表明$T$必须不完备。我们将其作为一个开放问题,即对于某些$T$,$g_T$的范围是否与所有无限的NP集相交(即是否是对于所有证明系统都很难的证明复杂度生成器)。一个命题版本的构造表明以下三个陈述中至少有一个是真的:-不存在p-最优命题证明系统(这等价于不存在时间最优的命题证明搜索算法),$E \not\subseteq P/poly$,存在一个把所有输入拉伸一位,可在次指数时间内计算的函数$h$,其范围$Rng(h)$与所有无限的NP集相交。