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集合相交。