关于哥德尔证明长度定理 I：
算术中的行数与加速

摘要

本文讨论了证明长度的下界，特别是以步数（推理次数）来衡量的下界。我们给出了哥德尔论断的第一个公开已知证明，即（i+1）阶算术相对于i阶算术存在超递归（实际上是无界的）证明加速，其中算术在希尔伯特风格的演算系统中形式化，使用 + 和 · 作为函数符号，或使用PRA的语言。同样的结果也适用于任何高阶逻辑的弱模式化形式系统；这允许所有重言式作为公理，并允许公理的所有泛化形式作为公理。

我们对哥德尔论断的第一个证明是基于自指句子；我们还给出了第二个证明，它避免了使用自指，该证明大致基于斯塔特曼（Statman）的方法。

1. 引言

本文提出了哥德尔关于证明长度的一个定理的第一个公开已知证明；本文的续篇将提出哥德尔关于证明长度的另一个论断的证明。哥德尔关于证明长度的第一个定理出现在他1936年的论文中，该定理指出，不存在任何递归函数可以限制(i+1)阶算术相对于i阶算术的证明加速。哥德尔关于证明长度的第二个定理出现在一封近期发现的致冯·诺依曼的信中；这封信中声称，一个图灵机，如果给定一个公式和一个整数n，能够确定该公式是否在一阶逻辑中有一个长度 ≤ n 个符号的证明，那么其运行时间必定会无限次地大于 ϵn 步，其中 ϵ 是某个常数。

我们对哥德尔这两个定理的证明使用了自指，并且推测这与哥德尔自己的证明方法相似。在本文中，我们还给出了第一个定理的一个证明，它避免了使用自指，部分基于斯塔特曼的方法。第二个定理的证明将在本文的续篇 [2] 中给出。

我们首先给出基本定义和本文的概述。i阶算术理论表示为 $Z_{i-1}$ —— 因此 $Z_0$ 是一阶皮亚诺算术，$Z_1$ 是二阶算术，以此类推。$Z_i$ 的非逻辑符号有 $0, S, +, ·$，并可选地包含所有原始递归函数的函数符号²。$Z_i$ 的通常公理包括：(1) 定义了 $0, S, +, ·$ 基本性质的鲁滨逊理论Q的公理，(2) 如果原始递归函数在 $Z_i$ 的语言中，则有定义它们的通用公理，(3) 对所有 $Z_i$ 的公式的归纳法，以及 (4) 如果 $i > 0$，则有对所有公式 $\phi$ 以及阶为 $j-1$ 和 $j \le i$ 的变量 $x$ 和 $X$ 的概括公理：

为了本文的目的，$Z_i$ 必须在一个希尔伯特风格的系统中形式化，而不是在Takeuti [16] 的Gentzen风格的 $G^1LC$ 中³。如果 $Z_i$ 的推理规则由Parikh [11]意义下的有限个模式集给出，那么我们就有了一个 $Z_i$ 的模式化公理化。对于模式化公理化，有效的推理规则由模式指定，任何公式、项和变量都可以代入这些模式以获得有效的推理规则，但需遵守关于变量名的句法条件。

模式化公理由没有前提的模式指定。然而，也存在非模式化的方式来指定公理：两个显著的例子是，所有（实例的）重言式都可以被允许作为公理，以及任何公理的全称量化（泛化）都可以被视为公理。如果 $Z_i$ 在一个希尔伯特风格的系统中形式化，其所有推理规则都由有限个模式集给出，除了公理也可能以重言式和通过任意泛化获得的形式给出，那么我们称 $Z_i$ 是弱模式化的。本文的所有方法都适用于 $Z_i$ 作为模式化或弱模式化系统。关于模式化和弱模式化证明系统的完整定义，请参见下文第2.3节。

因为我们允许弱模式化证明系统，其效果是本文的工作几乎适用于任何希尔伯特风格的 $Z_i$ 系统，例如，在Enderton、Mendelsohn、Kleene和Shoenfield的教科书中找到的证明系统。

定义

一个证明的符号长度（symbol-length）是证明中符号出现的总次数（包括变量下标中的符号，例如，在二进制表示法中）。

一个证明的步长（step-length）等于证明中公式的总数。步长显然也等于证明中公理和推理使用的总次数。

哥德尔 [6] 陈述了以下定理：

定理 1

对于 $i \ge 0$ 和任何递归函数 $h$，存在一个无限的 $\Pi^0_2$-公式族 $F$，使得对于任何句子 $\phi \in F$，$\phi$ 在 $Z_i$ 中是可证的，并且如果 $k$ 是 $\phi$ 的最短 $Z_{i+1}$-证明的步长，那么 $\phi$ 的最短 $Z_i$-证明的步长大于 $h(k)$。

在2.1节中，我们将使用一个自指公式来证明哥德尔定理的“符号长度”模拟，该公式表示“这个公式在 $\le f(x)$ 个符号内是不可证的”。这个定理可以在Mostowski [10] 和Ehrenfeucht-Mycielski [3] 中找到。

定理 2

设 $i \ge 0$ 且 $f$ 是任何递归函数。那么存在一个无限的 $\Pi^0_1$-公式族 $F$ 使得

• (1) 对于所有 $\phi \in F$，有 $Z_i \vdash \phi$，以及
• (2) 对于 $\phi \in F$，如果 $k$ 是使得 $Z_{i+1}$ 在 $k$ 个符号内证明 $\phi$ 的最小整数，那么 $Z_i$ 不可能在 $f(k)$ 个符号内证明 $\phi$。

尽管定理2是众所周知的，我们在此处仍包含一个证明，部分因为它是H. Friedman/Pudlák关于部分一致性陈述证明长度下界的一个很好的应用，部分是为了介绍证明定理1和3的一般方法。我们利用的Friedman/Pudlák结果包括对部分一致性陈述 $Con_T(f(n))$ 证明的符号长度的下界，该陈述指出理论 $T$ 没有符号长度 $\le f(n)$ 的 $0=1$ 的证明。

在2.2节中，我们证明了哥德尔定理的一个强化版本，对于以步数衡量的证明长度，给出了 $Z_{i+1}$ 相对于 $Z_i$ 的任意（而非递归）加速：

定理 3

设 $i \ge 0$。那么存在一个无限的 $\Pi^0_1$-公式族 $F$ 使得

• (1) 对于所有 $\phi \in F$，有 $Z_i \vdash \phi$，以及
• (2) 存在一个固定的 $k \in \mathbb{N}$ 使得对于所有 $\phi \in F$， $Z_{i+1}$ 在 $k$ 步内证明 $\phi$，以及
• (3) 不存在固定的 $k \in \mathbb{N}$ 使得对于所有 $\phi \in F$，$Z_i$ 在 $k$ 步内证明 $\phi$。

定理3显然意味着定理1对于任意函数 $h$ 都成立。定理3产生一个 $\Pi^0_1$-公式族而非 $\Pi^0_2$-公式族是基于马季亚谢维奇（Matijasevič）定理。

2.2节中定理3的证明使用了一个自指陈述，该陈述表示“这个公式在 $\le x$ 步内是不可证的”。然而，与2.1节的符号长度情况不同，我们无法获得部分一致性陈述步长的任何下界。为了在 $Z_i$ 被形式化为一个弱模式化系统时证明定理3（特别是当所有重言式都是 $Z_i$ 的公理时），我们必须在第3节中扩展Parikh和Krajíček的结果，这些结果根据证明的步长来限制证明中公式的逻辑复杂度。

Statman [15] 为具有无限模型的一阶模式化理论给出了类似的无界证明加速。在第3节中，我们重构了他的证明，去掉了理论具有无限模型的限制，并允许弱模式化理论，同时也允许高阶逻辑。这为定理3提供了一个避免使用自指的替代证明。

我们对定理3的证明给出了哥德尔定理（定理1）的第一个已知证明（除了推测哥德尔本人之外），该证明适用于高阶算术的所谓希尔伯特风格公理化，其中加法和乘法被视为函数符号。在 $Z_i$ 最多只有一个一元函数符号且没有非一元函数符号（因此加法和乘法是三元关系符号）的情况下，Parikh [11] 已对 $i=0$ 证明了定理3，Krajíček [7] 已对 $i > 0$ 证明了定理3。Parikh的证明使用了下文定理6的一个前身和克雷塞尔（Kreisel）猜想；Krajíček使用了Parikh的定理6前身的一个强化版本和对角化论证。基于自指陈述的Kreisel-Wang [9] 的方法可以很容易地扩展到证明定理3对于高阶算术的ε-演算形式化的类似物。关于此问题的先前工作的更多讨论可以在[12]中找到。

我要感谢Jan Krajíček提出的有益建议和评论。此外，我感谢Daniel Leivant的广泛讨论。

2. $Z_{i+1}$ 相对于 $Z_i$ 的证明加速

在2.1节中，我们证明定理2，这是哥德尔证明长度定理的模拟，其中证明长度由证明中的符号数量来衡量。2.1节的展开是通过使用Pudlák和H. Friedman对部分自洽性证明长度的下界来完成的。这为定理2提供了一个非常令人满意的证明。在2.2节中，证明了定理3，它涉及由步数衡量的证明长度。处理这种由步数衡量证明长度的情况更为困难，我们不知道相应的关于部分一致性证明长度的下界是否对由步数衡量的证明长度成立。相反，定理3是通过直接使用自指公式来证明的。为了完成定理3的证明，我们必须获得证明中公式的逻辑复杂度关于证明步数的上界；这在2.3节中针对弱模式化证明系统进行。

定义

设T是一个理论，φ是一个公式。我们用 $T \vdash_k \text{steps} \phi$，或有时仅用 $T \vdash_k \phi$，来表示存在一个φ的T-证明，其步数 ≤k。

我们用 $T \vdash_k \text{symbols} \phi$，或有时仅用 $T \vdash_k \phi$，来表示存在一个φ的T-证明，其符号数 ≤k。

定义

对于一个公式φ或一个项t，|φ|或|t|表示φ或t中的符号数量。对于一个证明P或证明的哥德尔数w，|P|或|w|表示证明中的符号数量。我们也用|n|表示整数n的二进制表示的长度。（这为w是哥德尔数的情况创造了两个定义|w|；通过高效的编码技术，这两个定义是多项式相关的，并且在任何情况下，上下文都会指明意图是哪个定义。）

2.1 符号长度加速

我们此后将用T表示一个可公理化的、一致的算术理论，其语言包含+（加法）和·（乘法）作为函数符号。该语言还可以包含其他函数符号，如后继S和可能的基本递归函数的符号。我们将假定T足够强大，可以有效地算术化元数学，例如，我们假定T（通过定义扩展）包含有界算术理论 $S_2^1$ 或 $I\Delta_0+\Omega_1$ 之一（关于这些有界算术的描述，请参见Buss [1] 和 Wilkie-Paris [17]）。对于 $n \ge 0$，$\underline{n}$ 表示一个值为n的闭项。由于+和·是函数符号，我们可以通过定义 $2\underline{n}$ 为 $(2 \cdot \underline{n})$ 和定义 $2\underline{n}+1$ 为 $(2 \cdot \underline{n}+1)$ 来确保 $|\underline{n}|$ 是 $O(\log n)$。

由于T是可公理化的，它有一个公理化系统，其公理在多磁带图灵机上是多项式时间可识别的。我们为T固定这样一个公理化系统。例如，T的公理可以由一个有限的公理模式集给出。

定义

$Con_T(x)$ 是一个一阶公式，表示T的部分一致性陈述，即不存在符号长度 ≤x 的T-证明证明出 $0=1$：

定理 4 (Pudlák [13, 14], H. Friedman)

设T是如上所述的一个算术理论。那么存在一个 $\epsilon > 0$，使得对于所有 $n > 0$，

证明 (简述)

根据哥德尔对角引理，存在一个公式φ使得

实际上，哥德尔对角引理的通常陈述仅适用于句子，但很容易看出，对角引理也适用于带有自由变量x的公式。现在 $\phi(x)$ 的形式是 $\neg(\exists w)\psi(w, x)$，其中 $\psi$ 是一个 $\Delta_1^b$-公式（因此也是一个 $\Sigma_1^b$-公式），它表示w是公式 $\phi(x)$ 的一个符号长度 $\le x$ 的证明的哥德尔数。根据Buss [1]的定理7.4或Wilkie-Paris [17]的定理6.4，存在一个多项式 $p(n)$ 使得

其基本思想是，如果 $\psi(w, x)$ 为真，那么T可以通过一个多项式大小的直接证明来证明 $\psi(w, x)$。（注意，如果 $\psi(w, x)$ 成立，则 $|w| \ge |\phi(x)| > |x|$；因此长度界限 $p(|w|)$ 不需要依赖于 $|x|$。）由于序列被假定在T中得到有效编码，T也证明了 $\psi(w, x) \rightarrow |w| \le k \cdot x$ 对于某个常数k成立。因此存在一个常数 $b > 0$ 使得

另一方面，(1) 意味着

结合(2)和(3)，我们得到

对于某个常数 $c \in \mathbb{N}$。取 $\epsilon < 1/c$。令 $m > 0$ 且 $n = m^c$，并为寻求矛盾而假设

现在，对于所有 $m \in \mathbb{N}$，

这由[1]的引理7.5或[17]的引理6.3得出。直观上，(6)的证明是通过注意到T可以使用定义符号S、+和·的公理，通过多项式大小的证明来证明像 $S(\underline{m}) = \underline{m+1}$，$ \underline{m+r} = \underline{m+r}$ 和 $\underline{m \cdot r} = \underline{m \cdot r}$ 这样的事实；形式上，这是首先通过对m的长度进行归纳来为S建立，然后为+，再为·建立。

从(6)可以轻易得出

因此，通过(4)、(5)和(7)，

对于足够大的m，$(m^c)^\epsilon + |\underline{m}|^{O(1)} \le m$，因此 $T \vdash_m \phi(\underline{m})$。但这样T根据φ的定义也证明了 $\neg\phi(\underline{m})$，这与T的一致性相矛盾。

我们已经证明了对于足够大的m，对于某个 $m \in \mathbb{N}$，当 $n = m^c$ 时，$T \vdash_{n^\epsilon \text{ symbols}} Con(\underline{n})$ 不成立。为了对不具 $m^c$ 形式的任意n建立这一点，我们注意到对于足够大的n，有 $n \le \lceil n^{1/c} \rceil^c \le 2n$。由此以及对于 $n' \ge n$，$T \vdash_{|n'|^{O(1)}} Con_T(\underline{n'}) \rightarrow Con_T(\underline{n})$ 的事实，我们得到对于所有足够大的n和某个常数 $\epsilon' \le \epsilon$，有 $\neg T \vdash_{n^{\epsilon'}} Con_T(\underline{n})$。如有必要，可取更小的 $\epsilon'$，使之对所有 $n > 1$ 都成立。

定理4证毕.

定理4可用于在 $Z_{i+1}$ 和 $Z_i$ 之间建立指数级加速；为了建立任意递归加速，我们如下推广部分一致性陈述 $Con_T$。

定义

一个部分递归函数 $f$ 是时间可构造的 (time constructible) 当且仅当存在一个图灵机 $M_f$，使得对于所有x，

我们定义 $f(x) \ge y$ 意味着 $M_f(x)$ 不在 < y 步内停机。注意，当 $f(x)$ 不收敛时，$f(x) \ge y$ 将成立。按照约定，每个时间可构造函数 $f$ 都满足 $f(x) \ge |x|$；图灵机 $M_f$ 将被明确构造成读取其全部输入，这迫使 $f(x) \ge |x|$，因为以二进制表示法输入的x长度为|x|。

显然，每个部分递归函数都被一个时间可构造函数所主导。注意，$f(x) \ge y$ 是一个递归谓词，实际上，$f(x) \ge |y|$ 是x和y的一个多项式时间谓词。

定义

$Con_T(f(x))$ 是一个带有自由变量x的 $\Pi_1^0$-公式，表示

定理 5

设T是如上所述的一个算术理论。那么存在常数 $\epsilon > 0$ 和 $c \in \mathbb{N}$，使得如果 $f$ 是一个时间可构造函数，则对于所有足够大的n，

当 $f(n)$ 未定义时，T根本不证明 $Con_T(f(n)^c)$。这里 $Con_T((f(n))^c)$ 应被解释为公式 $Con_T(g(n))$，其中g是时间可构造函数 $g(x) = f(x)^c$。对于许多理论T，c可以是一个小整数，如2或3，而 $\epsilon$ 可以是任何小于1的常数。

证明

定理5的证明与定理4的证明非常相似，所以我们只指出主要区别，并将细节留给读者。首先，让 $\phi(x)$ 现在是哥德尔对角公式，使得

现在，存在一个多项式p，使得

多项式p依赖于f（或者说，依赖于时间构造f的图灵机）；然而，p的次数与f无关。因此，取一个大于p的次数的 $a \in \mathbb{N}$，我们有在(8)中的 $p(|x|+y)$ 可以被替换为 $(|x|+y)^a$ 对于足够大的x, y；即，存在一个常数C，使得

将此与前一个证明的推理相结合，表明

对于某个常数b，它像a一样，与f无关。因此，存在一个常数 $c \in \mathbb{N}$，与f无关，使得

另一方面，我们有，对于某个 $\epsilon < 1$ 和所有足够大的n，如果

那么T将在 $\le f(n)$ 个符号内证明 $\phi(n)$。如前所述，这是一个矛盾，因为那样的话 $T \vdash \neg\phi(n)$。

定理5证毕.

我们现在准备证明哥德尔定理的类似物，其中证明长度用符号数代替步数。

定理 2 (重述)

设 $i \ge 0$ 且f是任何递归函数。那么存在一个无限的 $\Pi_1^0$-公式族F使得

• (1) 对于所有 $\phi \in F$, $Z_i \vdash \phi$, 以及
• (2) 对于 $\phi \in F$，如果k是使得 $Z_{i+1}$ 在k个符号内证明 $\phi$ 的最小整数，那么 $Z_i$ 不可能在 $f(k)$ 个符号内证明 $\phi$。

证明

回想一下，$Z_i$ 和 $Z_{i+1}$ 可以被视为模式化理论或弱模式化理论（完整定义见第3节）。很容易看出，这些理论的模式化版本相对于非模式化版本最多只有指数级加速；因此，为 $Z_i$ 和 $Z_{i+1}$ 的模式化版本证明定理2就足够了。这是幸运的，因为前两个定理依赖于T有一个多项式时间可识别的公理集。

设c和 $\epsilon$ 是适用于（模式化）理论 $T=Z_i$ 的定理5中的常数。不失一般性， $1/\epsilon$ 是一个整数且对于所有x，$f(x) \ge x$，并且f是一个时间可构造函数。设h是时间可构造函数 $h(x) = (f(x))^{1/\epsilon}$。设F是公式集合

对于 $n \ge 1$。我们必须证明三件事来建立这个定理：

• (1) 对于所有n，$Z_i \vdash Con_{Z_i}((h(\underline{n}))^c)$。
  对于一个固定的 $n \ge 1$，$Z_i$ 可以通过明确验证构造h的时间图灵机的执行来证明 $h(\underline{n}) = h(n)$。然后 $Z_i$ 可以检查所有有限多个符号数 $\le h(n)$ 的 $Z_i$-证明，以验证其中没有一个是 $0=1$ 的有效 $Z_i$-证明。
• (2) 对于所有足够大的n，$Z_i \vdash_{f(n)} Con_{Z_i}((h(\underline{n}))^c)$ 不成立。
  这直接由定理5得出。我们可以从F中丢弃n不够大的陈述 $Con_{Z_i}((h(\underline{n}))^c)$。
• (3) 对于所有n，$Z_{i+1} \vdash_{O(\log n)} Con_{Z_i}((h(\underline{n}))^c)$。
  使用(i+1)阶公式的真值定义，$Z_{i+1}$可以证明 $Z_i$ 的一致性，即，$Z_{i+1}$可以证明 $(\forall x)Con_{Z_i}(x)$。由此，$Z_{i+1}$ 容易推断出 $(\forall x)Con_{Z_i}((h(x))^c)$。现在 $|\underline{n}| = O(\log n)$，所以通过使用一个 $\forall$-实例化推理，$Z_{i+1} \vdash_{O(\log n)} Con_{Z_i}((h(\underline{n}))^c)$。

定理2直接从(1)、(2)和(3)得出。

证毕.

2.2 步长加速

我们接下来证明哥德尔定理的原始陈述，其中证明长度以步数而非符号数来衡量。使用符号长度来衡量证明是方便的，因为对于给定的符号长度，只有有限数量的证明，并且很容易枚举所有这些证明。然而，当使用步长时，情况就更困难了，因为对于给定的步长，很可能存在无限多个证明。这个复杂的因素确实提供了一个优势：我们将通过获得 $Z_{i+1}$ 相对于 $Z_i$ 的无界加速来改进哥德尔所陈述的定理。

由于我们无法限制给定步长的证明数量，因此对我们来说，转而限制证明中出现公式的逻辑复杂度将变得很重要，这需要根据证明的步长来衡量。为此，我们扩展了Parikh的一个构造，使其适用于仅仅是弱模式化的理论。

定义

如果φ是一个公式，其逻辑深度，记为dp(φ)，是φ中逻辑连接词嵌套的最大深度。对于原子公式φ，dp(φ)为0；对于形如(Qx)ψ或¬ψ的φ，dp(φ) = dp(ψ) + 1；对于φ = (ψ ⊙ χ)，其中⊙是一个二元连接词，dp(ψ)是1 + max{dp(ψ), dp(χ)}。

φ的量词深度或q-深度，记为q-dp(φ)，定义为φ中量词嵌套的最大深度。

ψ的量词块深度或qb-深度，记为qb-dp(ψ)，定义为ψ中同类量词块嵌套的最大深度。布尔连接词不增加qb-深度，如果φ是(Q⃗x)ψ，其中(Q⃗x)表示一个量词块，其中的量词要么都是存在量词，要么都是全称量词，并且ψ不以同类型的量词开头，那么qb-dp(φ) = 1 + qb-dp(ψ)。

定理 6

设T是一个弱模式化理论，并假设 $T \vdash_k \text{steps} \phi$。那么，存在一个φ的T-证明P，其步长 ≤k，使得P中的每个公式的量词块深度 ≤ qb-dp(φ) + O(k)。

O(k)中隐含的常数当然取决于理论T。定理6的证明推迟到2.3节；实际上，我们在那里证明了这个定理的一个强化版本。通过审视定理6的证明，将会很明显地看到 $I\Delta_0 + \exp$（因此对于 $i \ge 0$ 的 $Z_i$）可以证明这个定理的算术化版本——这对于我们证明下面这个哥德尔定理的强化形式至关重要：

定理 3 (重述)

设 $i \ge 0$。那么存在一个无限的 $\Pi_1^0$-公式族F使得

• (1) 对于所有 $\phi \in F$，有 $Z_i \vdash \phi$，以及
• (2) 存在一个固定的 $k \in \mathbb{N}$ 使得对于所有 $\phi \in F$， $Z_{i+1}$ 在k步内证明 $\phi$，以及
• (3) 不存在固定的 $k \in Z_i$ 使得对于所有 $\phi \in F$，$Z_i$ 在k步内证明 $\phi$。

证明

设 $i \ge 0$。令 $\phi(x)$ 是通过哥德尔对角化得到的公式，使得 $Z_0$ 证明

令 $F = \{\phi(n) : n \ge 0\}$。我们必须证明三个事实：

• (1) 对于所有 $n \ge 0$，不成立 $Z_i \vdash_n \phi(n)$。
  这直接源于 $Z_i$ 的一致性，因为如果 $Z_i \vdash_n \phi(n)$，那么 $Z_i$ 就能证明这个事实，从而 $Z_i \vdash \neg\phi(n)$。
• (2) 对于 $n \ge 0$, $Z_i \vdash \phi(n)$。
  为证明此点，固定一个 $n \ge 1$ 并在 $Z_i$ 中进行非形式化推理。首先，假设 $\neg\phi(n)$；那么 $Z_i \vdash_n \phi(n)$。根据定理6（可在 $Z_i$ 中形式化），可得存在一个 $\phi(n)$ 的 $Z_i$-证明，其中每个公式的qb-深度 $\le d \cdot n$（d为某个常数）。现在，$Z_i$ 有一个真值定义谓词 $Tri_{d \cdot n}^i$，用于qb-深度 $\le d \cdot n$ 的公式（必然地，$Tri_{d \cdot n}^i$ 的qb-深度 $> d \cdot n$）。这个真值谓词 $Tri_{d \cdot n}^i(\lceil\psi\rceil, x^i)$ 接受一个qb-深度 $\le d \cdot n$ 的公式 $\psi$ 的哥德尔数和一个阶为 $i+1$ 的元素 $x^i$，并将 $x^i$ 解释为对 $\psi$ 中所有自由变量的赋值编码，并给出在这些赋值下 $\psi$ 的真值。因此，$\psi$ 的有效性可以表示为：
  $$ Valid_i^{d \cdot n}(\lceil\psi\rceil) \equiv \forall x^i Tri_{d \cdot n}^i(\lceil\psi\rceil, x^i) $$
  此外，如同部分真值谓词的通常情况，$Z_i$ 可以证明所有qb-深度 $\le d \cdot n$ 的 $Z_i$ 公理在 $Tri_{d \cdot n}^i$ 的意义下都是有效的，并且推理规则保持有效性。因此，$Z_i$ 证明了如果 $Z_i \vdash_n \phi(n)$，那么 $Valid_i^{d \cdot n}(\lceil\phi(n)\rceil)$。进一步地，$Z_i$ 证明了 $Valid_i^{d \cdot n}(\lceil\phi(n)\rceil)$ 蕴含 $\phi(n)$ 成立（通过对 $\phi$ 的复杂度进行归纳）。因此，我们已经表明 $Z_i$ 证明了 $\neg\phi(n)$ 蕴含 $\phi(n)$；即，$Z_i \vdash \phi(n)$，证毕。
• (3) 存在一个 $k \ge 0$，使得对于所有 $n \ge 0$， $Z_{i+1} \vdash_k \phi(n)$。
  要确立这一点，只需证明 $Z_{i+1} \vdash (\forall x)\phi(x)$ 即可；因为从 $(\forall x)\phi(x)$ 可以用一个与n无关的常数数量的推理步骤推导出公式 $\phi(n)$。证明 $Z_{i+1} \vdash (\forall x)\phi(x)$ 的论证与上述(2)的论证类似；然而，定理6不再是必需的，因为 $Z_{i+1}$ 可以为 $Z_i$ 语言中的所有公式定义一个真值谓词。

定理3证毕.

定理3的证明在精神上与定理2的证明相似；然而，一个重要的区别是定理3的证明使用了一个哥德尔句子 $\phi$，该句子表达了自身在有界步数内的不可证性，而定理2的证明则使用了一个部分一致性陈述，断言了在有界符号数内 $0=1$ 的不可证性。一个有趣的问题是，定理3是否也能用部分一致性陈述来证明。这引出了一个本身就非常有趣的问题。令 $Con_{Z_i}(k \text{ steps})$ 表示公式 $\neg(Z_i \vdash_k \text{steps} 0=1)$：

问题

对于所有常数 $0 < \epsilon < 1$，是否对于所有足够大的n，都有 $Z_i \vdash_{n^\epsilon \text{ steps}} Con_{Z_i}(n \text{ steps})$ 成立？更一般地，$Con_{Z_i}(n \text{ steps})$ 的 $Z_i$-证明的最短步长是多少？甚至，是否存在一个常数k，使得对于所有n，都有 $Z_i \vdash_k Con_{Z_i}(n \text{ steps})$？

如果克雷塞尔猜想（Kreisel's conjecture）对于 $Z_i$ 所使用的特定形式化系统成立，那么最后一个问题的答案必须是“否”；然而，我们希望有一个自指的（self-referential）反证（当然，假设它是错误的）。我们所说的“克雷塞尔猜想”是指这样一个陈述：对于所有公式A(x)，如果存在一个固定的k，使得对于所有n，都有 $Z_i \vdash_k A(n)$，那么 $Z_i \vdash \forall x A(x)$。克雷塞尔猜想蕴含最后一个问题的答案为“否”的原因是，否则 $Z_i$ 将会证明其自身的一致性。

另一方面，我们有以下这个理论的例子，它不满足克雷塞尔猜想，并且其部分自洽性陈述没有 $o(n)$ 步长的证明：令 $\tilde{PA}$ 为皮亚诺算术的一阶理论，其公理包括通常的公理，外加所有形如 $m+n=m+n$ 和 $m \cdot n = m \cdot n$ 的真陈述。如果公式 $Con_{\tilde{PA}}(n \text{ symbols})$ 以形如 $(\exists \vec{x})(p(n, \vec{x}) = q(n, \vec{x}))$ 的形式表述，其中p和q是多项式，那么对于所有整数n，它们都有常数长度的 $\tilde{PA}$-证明。因此，克雷塞尔猜想对 $\tilde{PA}$ 不成立，否则 $\tilde{PA}$ 将证明其自身的一致性。另一方面，选择一个对角公式 $\phi(x)$ 使得

并让 $\neg\phi(x)$ 等价于一个形如 $\exists \vec{y}(p(x, \vec{y}) = q(x, \vec{y}))$ 的公式，其中p和q是多项式。根据 $\phi$ 的定义，$\tilde{PA}$ 证明

并且，根据 $\neg\phi$ 的形式，存在一个常数 $\ell$，使得 $\tilde{PA}$ 证明

因此 $\tilde{PA}$ 证明 $Con_{\tilde{PA}}(x + \ell' \text{ steps}) \rightarrow \phi(x)$，对于某个常数 $\ell'$。现在如果 $\tilde{PA}$ 能够以 $o(n)$ 步长的证明来证明其部分自洽性陈述，那么就可得出 $\tilde{PA}$ 能够以 $o(m)$ 步来证明每个公式 $\phi(m)$ ——这是一个矛盾。同样的推理表明，$\tilde{Z}_i$ 也不能以 $o(n)$ 步来证明其部分自洽性陈述 $Con_{\tilde{Z}_i}(n \text{ steps})$。

上述第一个问题是受Pudlák [13, 14]工作的启发，他在其中展示了PA中 $Con_{PA}(n \text{ symbols})$ 证明的符号长度的 $O(n^\epsilon)$ 下界。作为类比，我们猜想这个问题的答案是“否”，但目前的技术似乎不足以证明这一点。Pudlák还展示了这些证明符号长度的近线性上界。正如J. Krajíček指出的那样，同样的方法也足以证明 $Z_i$ 具有 $Con_{Z_i}(n \text{ steps})$ 的 $O(n)$ 步长证明。要证明这一点，注意到 $Z_i$ 可以形式化定理6并证明

对于某个常数c，其中 $I\Sigma_{cx+c}^i$ 表示限制在 $\Sigma_{cx+c}^i$-公式上进行归纳的理论 $Z_i$。现在，对于 $m \ge 0$，$Z_i$ 可以为 $\Sigma_m^i$-公式给出一个部分真值定义，并在 $O(m)$ 行内证明它满足通常的性质。然后 $Z_i$ 可以在 $O(n)$ 步内证明 $Con_{I\Sigma_{cn+c}^i}(n \text{ steps})$，因此也证明了 $Con_{Z_i}(n \text{ steps})$。

另一个观察，Krajíček也向我们指出，是关于 $Z_i$ 的形式化，其中后继函数S是唯一的函数符号（允许+、·等作为关系符号）。在这种情况下，如果 $Z_i \vdash_k Con_{Z_i}(n \text{ steps})$，那么对于某个取决于 $Z_i$ 形式化的常数d，有 $k \ge d \log \log n$。这是通过使用[7]的定理3.1来证明的，该定理暗示如果 $Z_i \vdash_k Con_{Z_i}(n \text{ steps})$，则 $Z_i \vdash_{(log n)^{2^{2^{O(k)}}}} Con_{Z_i}(n \text{ steps})$，因此 $Z_i \vdash_{(log n)^{2^{2^{O(k)}}}} Con_{Z_i}(n \text{ symbols})$。然后Pudlák-Friedman下界意味着 $(\log n)^{2^{2^{O(k)}}} > n^\epsilon$ 对于某个 $\epsilon > 0$；由此得出 $k = \Omega(\log \log n)$。

开放问题

另一个开放问题是，是否存在一个关于 $Z_{i+1}$ 相对于 $Z_i$ 的“无加速”结果。即，是否存在一个 $Z_{i+1}$ 的推论的无限集合 $\{\phi_j\}_j$ 和一个适度增长的函数g，比如 $g(j)=2^j$，使得如果 $k_j$ 是 $\phi_j$ 的一个 $Z_{i+1}$-证明的最小步长，那么以下成立：(1) $k_j \ge g(|\phi_j|)$ 并且 (2) $Z_i \vdash_{k_j} \phi_j$ 也成立？使用符号长度的相应问题也同样是开放的。

2.3 通过步长限制公式复杂度

一个公式φ完全有可能存在一个步长为k的证明P，但P中的公式却具有任意大的逻辑复杂度。这有多种原因，最明显的是，P可能包含公理，例如形如 $A \rightarrow (B \rightarrow A)$ 的重言式，其中包含具有任意高逻辑复杂度的子公式。然而，我们将在下面看到，通过证明只要 $T \vdash_k \text{steps} \phi$（其中T是一个弱模式化理论），就存在一个φ的T-证明，其中每个公式的逻辑复杂度（qb-深度）都受φ的复杂度加上 $O(k)$ 的限制，从而可以避免这种高逻辑复杂度。

首先，我们正式定义什么是模式化（schematic）和弱模式化（weakly schematic）理论。Parikh [11] 是第一个引入模式化理论的。

表示法

i阶逻辑的语言包含j+1阶（$j+1 \le i$）的变量 $x_j$（通常仅记为x，不带表示阶数的上标）、常量符号（我们假设0是一个常量符号）、函数符号（如S, +, ·）、各种关系符号（包括=和∈），以及由布尔连接词和量词 $\forall x_j$ 和 $\exists x_j$ 组成的逻辑连接词。函数符号必须接受一阶参数并产生一阶值。除=和∈外的关系符号也只接受一阶参数。

我们称一个对象为j类型（type j）当且仅当它的阶为j+1；因此，$x^j$ 中的上标指的是变量的类型。

为了以模式化的方式指定公理和推理规则，我们需要用于i阶逻辑语法的元表示法。因此，存在：

• (i) j类型的元变量（metavariables）$\alpha_j$，它代表j类型的变量。
• (ii) 项变量（term variables）$\sigma, \tau, \ldots$，它代表（0类型的）项。
• (iii) 不同元数的公式变量（formula variables）$A(x_1), B(x_1, x_2), \ldots$，它代表公式。

元项（Metaterms）由变量、元变量、常量、函数符号和项变量构成。

一个原子元公式（atomic metaformula）由一个应用于元项的公式变量或一个应用于元项的谓词符号组成。

元公式（Metaformulas）由原子元公式通过布尔连接词和量词构成；我们常用大写希腊字母 $\Phi, \Psi, \ldots$ 来表示元公式。

一个代换（substitution）S包含一个从元变量到元变量的映射，从项变量到项的映射，以及从公式变量到公式的映射。我们用 $\kappa^S$ 表示S将元符号 $\kappa$ 映射到的值。代换S可以扩展为一个从元项和元公式到项和公式的映射。如果 $\Phi$ 是一个元公式，S是一个代换，那么公式 $\Phi^S$ 是通过将 $\Phi$ 中的每个元符号 $\kappa$ 替换为 $\kappa^S$ 得到的结果。对于 $\kappa$ 是一个元变量或项变量的情况，这很容易定义；对于 $\kappa$ 是一个公式变量，形如 $A(u_1, \ldots, u_k)$，我们定义 $(A(s_1, \ldots, s_k))^S$ 为通过将项 $s_1^S, \ldots, s_k^S$ 代入公式 $\kappa^S$ 中所有自由出现的变量 $u_1, \ldots, u_k$ 而得到的公式（这里，$s_i$ 是元项）。这最后一个定义即使在 $s_i^S$ 不能自由地代入 $\kappa^S$ 中的 $u_i$ 时也适用；然而，可以构造弱模式化系统来避免代换不自由的情况（事实上，高阶算术的弱模式化系统总会有明确排除代换不自由可能性的“附加条件”）。变量 $u_1, u_2, \ldots$ 可以是任何指定的0类型变量列表。关于元公式和代换的更全面的定义，请参见Farmer [5]。

形式上，一个代换S必须是全射的，即S为所有元符号赋值；但显然，公式 $\Phi^S$ 只依赖于 $\Phi$ 中出现的元符号 $\kappa$ 的值 $\kappa^S$。因此，使用部分代换将是有用的。一个更普遍的概念是元代换（metasubstitutions）：元代换的定义与代换类似，只是元代换将元变量映射到元变量和变量，将项变量映射到元项，将公式变量映射到元公式。如果S是一个元代换，$\Phi$ 是一个元公式，那么 $\Phi^S$ 的定义是显而易见的。

两个元代换的复合（composition），记为 $S \circ S'$ 或 $SS'$，是通过先应用S再应用S'来计算的。

定义

一个理论T是模式化的（schematic）当且仅当以下条件成立：

• T中的证明由一系列公式组成，其中每个公式都是通过推理规则从前面的公式推导出来的。
• 推理规则由一个有限的模式集合给出：
  $$ \frac{\Phi_1, \ldots, \Phi_k}{\Psi} \quad (R) $$
  其中 $\Phi_1, \ldots, \Phi_k, \Psi$ 是元公式，R是一个有限的附加条件集合（见下文允许的附加条件）。一个有效的推理形如：
  $$ \frac{\Phi_1^S, \ldots, \Phi_k^S}{\Psi^S} $$
  其中S是一个满足条件 $R^S$ 的代换。

R中的附加条件可以是以下四种形式之一：

其中 $\alpha_j, x_j, s$ 可以是任何j类型的元变量、j类型的变量或元项（分别地），而 $\Phi$ 是一个元公式。

许多（但绝非全部）i阶逻辑的形式系统是模式化的。模式化推理规则的例子有：

• 分离规则 (Modus Ponens):
  $$ \frac{\Phi_1, \Phi_1 \rightarrow \Phi_2}{\Phi_2} $$
  （无附加条件）
• 全称实例化规则 (Universal Instantiation Rule):
  $$ \frac{\forall \alpha_j A(\alpha_j)}{A(\tau^j)} $$
  要求 $\tau^j$ 在 $A(\alpha_j)$ 中可自由地代换 $\alpha_j$。
• 全称实例化公理 (Universal Instantiation Axiom):
  $$ / \forall \alpha_j A(\alpha_j) \rightarrow A(\tau^j) $$
  同样的附加条件。
• 概括公理 (Comprehension Axiom):
  $$ / \exists \alpha_{j+1} \forall \beta_j (\beta_j \in \alpha_{j+1} \leftrightarrow A) $$
  要求 $\alpha_{j+1}$ 在 A 中不是自由的。

在最后两个例子中，推理没有前提（即，它们是公理）。回想一下，在我们证明哥德尔定理（或定理3）时，我们使用了理论具有某种模式化形式的全称实例化规则或公理的假设。

然而，事实证明，许多理论并非模式化的，因为它们拥有无法被有限个模式列表所捕获的公理或规则。一个理论可能不是模式化的两种常见方式是：该理论可能承认所有重言式为公理，以及该理论可能允许所有公理的泛化形式也为公理。（关于后者的一个例子，请参见Enderton [4]。）一个公式 $\phi$ 的泛化（generalization）指的是任何可以通过在 $\phi$ 前面加上全称量词得到的公式。

定义

一个理论T是弱模式化的（weakly schematic），如果T-证明由一系列公式组成，并且有效的推理规则由以下方式指定：

1. 一个有限的模式集合，如同模式化理论一样（零前提的推理是公理）。
2. 所有重言式都是公理。
3. 所有公理的泛化形式也都是公理。

然而，可以省略将所有重言式作为公理，或者只选择特定的公理使其所有泛化形式也成为公理；在这些情况下，我们仍然称该理论为弱模式化的。一个弱模式化理论，如果其中没有公理被选择使其所有泛化形式都成为公理，则称为无泛化的（generalization-free）。

我们现在可以陈述定理6的强化形式；(a)部分主要归功于Parikh [11]，并由Krajíček [7]以此处陈述的形式证明：

定理 7

• (a) 设T是一个模式化理论，并假设 $T \vdash_k \text{steps} \phi$。那么存在一个φ的T-证明P，其步长 ≤k，使得P中的每个公式的深度 ≤ dp(φ) + O(k)。
• (b) 设T是一个无泛化的、弱模式化的理论，并假设 $T \vdash_k \text{steps} \phi$。那么存在一个φ的T-证明P，其步长 ≤k，使得P中的每个公式的量词深度 ≤ q-dp(φ) + O(k)。
• (c) 设T是一个弱模式化的理论，并假设 $T \vdash_k \text{steps} \phi$。那么存在一个φ的T-证明P，其步长 ≤k，使得P中的每个公式的量词块深度 ≤ qb-dp(φ) + O(k)。

我们对定理7的证明基于Parikh的证明骨架（proof skeleton）和合一（unification）的概念。证明骨架是对一个潜在证明的部分描述；证明骨架通过指定使用了哪个推理规则或公理模式、哪些行被用作前提以及哪些变量被代入模式中的任何元变量，来告诉我们证明中的每个公式是如何推导出来的。如果一个公理被证明为重言式，那么证明骨架会给出该公理是哪个命题重言式的一个实例。如果该公理是重言式或公理模式的泛化，那么证明骨架不仅指定了该重言式或模式，还指定了整个全称量词块。然而，证明骨架并不指定推理模式中项变量和公式变量的实例化（这与证明骨架确实指定了哪些变量被代入元变量的事实形成对比）。

显然，每个证明都有一个证明骨架；然而，并非每个证明骨架都对应一个有效的证明。此外，不同的证明可能拥有相同的证明骨架。通过重命名项变量和公式变量，我们可以确保证明骨架对每个推理使用不同的项变量和公式变量。这样一个证明骨架对应于公式 $\phi$ 的一个证明，当且仅当存在一个代换S使得该骨架成为 $\phi$ 的一个证明；具体来说，(a) 对于骨架中最后一次推理的结论 $\Phi$，有 $\Phi^S = \phi$，以及 (b) S满足每次推理的附加条件，以及 (c) 每当证明骨架中的一个元公式 $\Psi$ 代表一个推理的结论，而证明骨架中的 $\Psi'$ 代表用作某个推理前提的相同公式时，有 $\Psi^S = \Psi'^S$。换句话说，一个证明骨架代表了一个合一问题，其解恰好是那些能将骨架转化为一个证明的代换。关于合一和证明骨架的更多讨论，请参见[11, 8, 7, 5]。

假设T是弱模式化的。给定一个步长为k的 $\phi$ 的T-证明P，令PS是其骨架；定理7(c)将通过证明存在一个具有相同骨架的T-证明P*，其中每个公式的qb-深度 ≤ qb-dp(φ) + O(k) 来建立。

首先，我们可以不失一般性地假设，出现在证明P中的每个变量都在骨架PS中被提及，因为否则，如果y是一个未在P中出现的变量，我们可以擦除P中出现的每个量词Qy，并用常量0替换y的其余（现在是自由的）出现。⁷

在P中，我们可以擦除P中出现的每个量词Qy，并用常量0替换y的其余（现在是自由的）出现。⁷

证明骨架PS对应于一个由一组形如 $\Phi = \Psi$ 的方程和一组限制（附加条件）组成的合一问题。我们必须证明存在一个满足方程和限制的代换S，使得S能导出一个$\phi$的证明，且证明中所有公式的qb-深度都受 qb-dp(φ) + O(k) 的限制。我们不关心限制证明中项的大小，因此我们只需要考虑限制S赋给元公式的公式大小；为此，我们只考察合一问题中对应于逻辑连接词的部分——这是一个所谓的一阶合一问题，可以用标准技术轻松解决：

断言

PS的合一问题有一个最一般公式解 (most general formula solution, mgfs)；即，存在一个元代换 $S_{mgfs}$，它将公式变量映射到元公式，但将项变量映射到自身，并且合一问题的任何其他解S都可以表示为 $S_{mgfs} \circ S'$ 的形式，其中S'是某个（元）代换。

此外，令D等于PS中所有公式中出现的量词块总数。那么对于PS中出现的所有元公式$\Phi$，$\Phi^{S_{mgfs}}$的qb-深度 $\le D$。

为了证明该断言，我们不失一般性地假设D中的每个方程都具有 $A = \Phi$ 的形式，其中A是一个0元公式变量（我们可以通过将D中的每个方程 $\Phi = \Psi$ 替换为两个方程 $A = \Phi$ 和 $A = \Psi$ 来确保这一点，其中A是一个新的公式变量）。我们将通过迭代修改方程集D来产生 $S_{mgfs}$，并创建一个新的方程集E。初始时，E是空集。对于D中出现的公式变量A和B，我们令 $A \sim B$ 表示D中存在一个方程 $A = B(\vec{t})$。令 $\approx$ 为 $\sim$ 的自反、传递、对称闭包。我们记 $A \succ_0 B$ 表示在D中存在一个形如 $A = \odot(\vec{\Psi})$ 的方程，其中B出现在$\vec{\Psi}$中，而$\odot$代表一个布尔连接词或一个量词。我们记 $A \succeq B$ 表示关系 $(A \approx B \lor A \succ_0 B)$ 的传递闭包。重要的是要强调，$\succeq$关系在修改D的迭代过程的每一步之后都会被重新定义。很明显，必定至少有一个变量相对于$\succeq$排序是极大的；因为D有一个解。

修改D和E的迭代过程如下：

选择一个在D中 $\succeq$-极大的任意A，使得D中存在一个形如 $A = \odot(\Psi_1, \ldots, \Psi_s)$ 的方程，其中$\odot$要么代表一个布尔连接词（此时s=1或s=2），要么是一个谓词符号（s≥1），要么是一个最大长度的同类量词块。（在最后一种情况下，s=1且$\Psi_1$不以同类型的量词开头。此外，“最大长度”指的是在所有对 $A = \odot(\vec{\Psi})$ 方程的选择中是最大的。）注意，$\Psi_1, \ldots, \Psi_s$ 是元公式，除非$\odot$是谓词符号；在这种情况下，$\Psi_1, \ldots, \Psi_s$ 是元项。令 $\vec{u}$ 是一个新的0类型变量的无限序列；当C是k元的，我们用 $C(\vec{u})$ 表示 $C(u_1, \ldots, u_k)$。现在，对每个0元公式变量 $B \approx A$，执行以下操作：

1. 选择 $B_1, \ldots, B_s$ 为新的公式变量，除非$\odot$是谓词符号，此时选择 $B_1, \ldots, B_s$ 为新的项变量。
2. 在D中找到每个形如 $B = \Psi$ 的方程。从D中移除此方程。将E中所有出现的公式变量B替换为方程 $\odot(B_1, \ldots, B_s)$。然后将公式 $B = \odot(B_1, \ldots, B_s)$ 添加到E中。
3. 对于在(b)中找到的每个方程 $B = \Psi$，如果$\Psi$等于 $C(\vec{t})$，其中C是一个公式变量，$\vec{t}$是元项，令 $C_1, \ldots, C_s$ 为与C具有相同元数的新公式变量，并将方程 $B_i = C_i(\vec{t})$ 添加到D中（对于i=1, ..., s）。找到E中所有出现的 $C(\vec{u})$ 并将其替换为 $\odot(C_1(\vec{u}), \ldots, C_s(\vec{u}))$；然后将方程 $C(\vec{u}) = \odot(C_1(\vec{u}), \ldots, C_s(\vec{u}))$ 添加到E中。
4. 现在考虑在(b)中找到的每个方程 $B = \Psi$，如果$\Psi$是 $\otimes(\Theta_1, \ldots, \Theta_{s'})$，其中$\otimes$是一个布尔连接词或谓词符号：如果$\otimes$不等于$\odot$，则合一问题无解，这与证明P存在并提供了一个解的事实相矛盾。由于$\otimes$和$\odot$相等，s'=s。将s个方程 $B_i = \Theta_i$ 添加到D中。
5. 现在考虑在(b)中找到的每个方程 $B = \Psi$，如果$\Psi$以一个量词块 $Q\vec{x}$ 开头。由于$\odot$被选为最大长度，并且存在合一问题的解，$\odot$由 $Q\vec{x}$ 后跟一个（可能为空的）相似量词列表 $Q\vec{y}$ 组成。在 $Q\vec{y}$ 为空列表的情况下，$\Psi$ 形如 $\odot\Theta$，将方程 $B_1 = \Theta$ 添加到D。否则 $Q\vec{y}$ 不为空，我们有$\Psi$ 形如 $Q\vec{x}C(\vec{t})$，其中C是一个公式变量；在这种情况下，将 $C' = C(\vec{t})$ 和 $C' = Q\vec{y}B_1$ 添加到D中，其中C'是一个新的公式变量。

当D中的所有方程都形如 $A = C(\vec{s})$ 时，这个迭代过程停止，其中A和C是公式变量。该过程最终必须停止，因为每次迭代都会减少D中逻辑连接词的总数。事实上，每次迭代都会从D中移除至少一个布尔连接词或量词块；并且最多向E中公式的深度增加一个（相同的）连接词或量词块。由此可见，E中公式的qb-深度受证明骨架PS中量词块总数的限制。此外，由于该过程的一步是在一个 $\succeq$-极大的A上执行的，很容易看出，在那一步之后，新的方程集D不包含任何A或任何 $B \approx A$ 的出现。

最后，$S_{mgfs}$可以定义如下：令E为上述过程最终迭代后得到的方程集。如果 $A(\vec{u}) = \Phi$ 是E中的一个方程，那么 $A^{S_{mgfs}}$ 定义为$\Phi$。如果$\kappa$没有出现在E中方程的左侧，则 $\kappa^S$ 就是$\kappa$本身。很容易检查 $S_{mgfs}$ 是良定义的；也很容易验证任何满足来自证明骨架的原始方程集和限制的代换S，都必须可以表示为 $S = S_{mgfs} \circ S'$ 的形式，其中S'是某个元代换。（后一个事实可以通过对创建E的过程的迭代次数进行归纳来证明。）

这就完成了该断言的证明。 定理7现在可以相对容易地被证明。回想一下，P被假设为$\phi$的一个k步T-证明，PS是其证明骨架。从PS我们构成了带有附加条件的合一问题D。D中，不失一般性地，有一个形如 $A = \phi$ 的方程，并且总共有O(k)个对应k步的方程。每个O(k)方程中出现的量词块数量受一个常数限制，因为只有有限数量的推理和公理模式。⁸

令 $S_{mgfs}$ 为断言中的最一般公式代换。由于D有 qb-dp($\phi$) + O(k) 个量词块，$S_{mgfs}$ 将公式变量映射到qb-深度 $\le$ qb-dp(A) + O(k) 的元公式。证明P是通过对PS应用某个代换S得到的，根据断言，$S = S_{mgfs} \circ S'$，其中S'是某个代换。问题在于S′可能会引入新的量词块，从而导致P中公式具有很高的qb-深度。

然而，我们可以用另一个不引入任何新量词块（或新布尔连接词）的代换S''来替换S'。S''定义如下：对于每个公式变量A，令 $A^{S'}$ 是一个公式，令 $P(s_1, \ldots, s_\ell)$ 是 $A^{S'}$ 的第一个（即最左边的）原子子公式，并假设 $P(\vec{s})$ 在 $A^{S'}$ 中处于量词 $Q_1y_1, \ldots, Q_ry_r$ 的作用域内。定义 $A^{S''}$ 为从 $P(\vec{s})$ 中通过将所有出现的 $y_1, \ldots, y_r$ 替换为常量符号0而得到的公式。对于所有不是公式变量的$\kappa$，令 $\kappa^{S''} = \kappa^{S'}$。

令 $P' = P^{S_{mgfs}S''}$ 是通过将代换 $S_{mgfs}S''$ 应用于骨架PS得到的证明。显然，P'中的每个公式的qb-深度 $\le$ qb-dp($\phi$) + O(k)。剩下的工作是证明 $S_{mgfs}S''$ 满足所有的附加条件，因为这样 P' 就是一个有效的证明。附加条件变为以下形式：

很容易检查，由于这些条件在 $P = P^S$ 中成立，它们在P'中也成立；即，如果x在 $\Phi^S = \Phi^{S_{mgfs}S'}$ 中不是自由出现的，那么它在 $\Phi^{S_{mgfs}S''}$ 中肯定也不是自由出现的，并且，如果 $\tau^S = \tau^{S'} = \tau^{S''}$ 可在 $\Phi^S = \Phi^{S_{mgfs}S'}$ 中自由代换x，那么它在 $\Phi^{S_{mgfs}S''}$ 中也可自由代换x。

定理7(c)证毕.

定理7的(a)和(b)部分可以类似地证明。只需将qb-深度分别替换为‘深度’和‘q-深度’，所有论证都只需稍作修改即可通过。

3. 无需自指的证明加速

在本节中，我们为哥德尔定理和定理3提供了一种避免使用自指的替代证明方法；这个证明几乎可以肯定不是哥德尔所设想的那种证明，而且与使用自指的证明不同，它从哲学（基础性）的角度来看有些令人失望。尽管如此，它为证明系统的局限性提供了重要信息。

本节的基本思想归功于斯塔特曼（Statman），下一定理也归功于他。我们的证明将基于定理7。

定理 8 (Statman [15])

设T是一个模式化理论，$\phi$是一个独立于T的公式。进一步假设 $T \cup \{\neg\phi\}$ 有一个无限模型。那么存在一个数m，使得对于每个k > 0，都存在一个重言式 $\psi_k$ 使得

• (1) $T \cup \{\phi\} \vdash_m \text{steps} \psi_k$,
• (2) $T \vdash \psi_k$, 以及
• (3) 不成立 $T \vdash_k \text{steps} \psi_k$。

我们将证明一个稍强版本的斯塔特曼定理，它适用于弱模式化理论；当然，在这种情况下，$\psi_k$ 不能再是重言式，因为弱模式化理论可能将所有重言式作为公理。我们还省略了 $T \cup \{\neg\phi\}$ 具有无限模型这个不必要的假设。

定理 9

• (a) 设T是一个弱模式化理论，$\phi$是一个T不可证的公式。那么存在一个数m，使得对于所有k > 0，都存在一个有效公式 $\psi_k$ 使得
  1. (1) $T \cup \{\phi\} \vdash_m \text{steps} \psi_k$,
  2. (2) $T \vdash \psi_k$, 以及
  3. (3) 不成立 $T \vdash_k \text{steps} \psi_k$。
• (b) 同样的结果对模式化理论T也成立，附加条件是 $\psi_k$ 是一个重言式。

注意(b)基本上是去掉了无限模型假设的定理8。

我们证明定理9的思路非常容易解释：为了证明(b)，取 $\psi_k$ 为公式 $\theta_k \lor \phi$，其中 $\theta_k$ 是公式

这里有k个 $\lor$ 符号，其中 $\top$ 是某个有效句子，如 $\forall x(x=x)$，而 $\bot$ 是 $\neg\top$。那么 $\psi_k$ 显然是一个重言式并且在T中可证；此外，$T \cup \{\phi\}$ 在常数行内证明 $\psi_k$。另一方面，我们将证明，如果 $\psi_k$ 在某个模式化理论S中有一个少于 $\epsilon k$ 行的证明（其中常数 $\epsilon$ 取决于S），那么 $S \vdash \phi$。这个断言背后的直观思想是，由于一个模式化系统在单个证明步骤中只能处理有限数量的嵌套 $\lor$，任何少于 $\epsilon k$ 行的 $\psi_k$ 的证明都必须通过证明$\phi$来进行。更正式地，我们将证明，任何少于 $\epsilon k$ 行的 $\psi_k$ 的证明都可以转化为 $\theta_k^\bot \lor \phi$ 的证明，其中 $\theta_k^\bot$ 是将 $\theta_k$ 中的 $\top$ 替换为 $\bot$ 的公式。但 $\theta_k^\bot \lor \phi \rightarrow \phi$ 显然是可证的，这就导致了矛盾。

(a)的证明思想类似，但现在取 $\theta_k$ 为公式

这里同样有k个 $\lor$ 符号。

为了使这个证明思想形式化，我们首先需要一个引理。我们说$\phi$和$\phi'$是逻辑相似的 (logically similar)，如果它们具有相同的逻辑结构（即，它们仅在原子子公式的选择上有所不同）。

引理 10

• (a) 设R是一个模式化的推理规则，并假设R中出现的每个元公式的逻辑深度≤D。设S是一个代换，使得 $R^S$ 是该规则的一个有效实例。设φ是一个公式，并假设在 $R^S$ 中所有与φ逻辑相似的子公式的出现都在深度>D处。那么，如果将 $R^S$ 中每个与φ逻辑相似的子公式的所有出现都替换为任意一个固定的句子ψ（例如⊤或⊥），那么就会得到该规则的另一个有效实例。
• (b) 假设R是一个弱模式化指定的公理，由一个元公式给出，可能带有附加条件，并且可以任意地进行全称量化。假设R及其附加条件中的每个元公式的逻辑深度≤D。设代换S和一个全称量词块指定了R的一个有效实例。设φ是一个不以全称量词开头的公式，并假设在 $R^S$ 中每个与φ逻辑相似的子公式的出现都在深度>D处。那么通过将 $R^S$ 中每个与φ逻辑相似的子公式的所有出现都替换为任意一个固定的句子ψ，就可以得到该规则的另一个有效实例。

证明

(a) 从S得到S'，方法是修改S，令对于非公式变量的κ，有 $\kappa^{S'} = \kappa^S$，并令 $\kappa^{S'}$ 为 $\kappa^S$，但其中每个与φ逻辑相似的子公式φ*都被替换为ψ。那么 $R^{S'}$ 是模式R的一个有效实例，因为附加条件很容易看出仍然满足，因为ψ是一个句子，没有自由出现的变量。

(b)部分的证明与此类似。

我们现在可以证明定理9(a)。由于T是一个弱模式化理论，其规则要么是模式化的，要么是模式化公理的泛化，要么是重言式的泛化。设D为T的规则中出现的元公式的最大逻辑深度，设c为S的任何弱模式化规则中出现的最大元公式数量。由于所有逻辑连接词的元数≤2，一个公式在深度≤D处最多可以有 $2^{D+1}-1$ 个子公式。因此，在一个k步的T-证明中，作为P中一个公式的深度≤D的子公式出现的公式少于 $k \cdot c \cdot 2^{D+1}$ 个。

设 $\theta_0$ 为 $\exists x(\top)$，$\theta_{i+1}$ 为 $\exists x(\bot \lor \theta_i)$。设 $\psi_k$ 为 $\theta_{kc2^{D+1}} \lor \phi$。现在假设P是$\psi_k$的一个步长≤k的T-证明。根据鸽巢原理，存在某个 $\ell < kc2^{D+1}$，使得在P中的任何公式中，都没有在深度≤D的子公式位置上出现 $\psi_\ell$ 或任何与 $\psi_\ell$ 逻辑相似的公式。因此，根据引理10，如果在P中将所有与 $\psi_\ell$ 逻辑相似的子公式的出现都替换为⊥，那么就会得到一个有效的T-证明P'。现在P'是 $\theta^\bot_{kc2^{D+1}-\ell} \lor \phi$ 的一个证明；由于第一个析取项是可证伪的，因此可得 $T \vdash \phi$。

我们已经证明，如果 $T \vdash_k \text{steps} \psi_k$，那么 $T \vdash \phi$。所以，如果φ不能被T证明，那么T就不可能在k步内证明 $\psi_k$。然而，$T \vdash \psi_k$ 因为 $\psi_k$ 是有效的。此外，很明显 $T \cup \{\phi\} \vdash_m \text{steps} \psi_k$，对于某个与k无关的常数m，因为 $\psi_k$ 包含φ作为一个析取项。这就证明了定理9(a)。

(b)部分的证明类似，但 $\theta_{kc2^{D+1}}$ 现在可以是重言式

其中有 $kc2^{D+1}$ 个 $\lor$ 符号。

参考文献

• [1] S. R. Buss, Bounded Arithmetic, Bibliopolis, 1986. Revision of 1985 Princeton University Ph.D. thesis.
• [2] S. R. Buss, On Gödel’s theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability, in Feasible Mathematics II, P. Clote and J. Remmel, eds., Birkhäuser-Boston, 1995, pp. 57–90.
• [3] A. Ehrenfeucht and J. Mycielski, Abbreviating proofs by adding new axioms, Bulletin of the American Mathematical Society, 77 (1971), pp. 366–367.
• [4] H. Enderton, A Mathematical Introduction to Logic, Academic Press, 1972.
• [5] W. M. Farmer, A unification-theoretic method for investigating the k-provability problem, Annals of Pure and Applied Logic, 51 (1991), pp. 173–214.
• [6] K. Gödel, Über die Länge von Beweisen, Ergebnisse eines Mathematischen Kolloquiums, (1936), pp. 23–24. English translation in Kurt Gödel: Collected Works, Volume 1, pages 396-399, Oxford University Press, 1986.
• [7] J. Krajíček, On the number of steps in proofs, Annals of Pure and Applied Logic, 41 (1989), pp. 153–178.
• [8] J. Krajíček and P. Pudlák, The number of proof lines and the size of proofs in first-order logic, Archive for Mathematical Logic, 27 (1988), pp. 69–84.
• [9] G. Kreisel and H. Wang, Some applications of formalized consistency proofs, Fundamenta Mathematicae, 42 (1955), pp. 101–110.
• [10] A. Mostowski, Sentences Undecidable in Formalized Arithmetic: An Exposition of the Theory of Kurt Gödel, North-Holland, 1952.
• [11] R. J. Parikh, Some results on the lengths of proofs, Transactions of the American Mathematical Society, 177 (1973), pp. 29–36.
• [12] R. J. Parikh, Introductory note to 1936(a), in Kurt Gödel, Collected Works, Volume 1, Oxford University Press, 1986, pp. 394–397.
• [13] P. Pudlák, On the lengths of proofs of finitistic consistency statements in first order theories, in Logic Colloquium ’84, North-Holland, 1986, pp. 165–196.
• [14] P. Pudlák, Improved bounds to the lengths of proofs of finitistic consistency statements, in Logic and Combinatorics, vol. 65 of Contemporary Mathematics, American Mathematical Society, 1987, pp. 309–331.
• [15] R. Statman, Speed-up by theories with infinite models, Proceedings of the American Mathematical Society, 81 (1981), pp. 465–469.
• [16] G. Takeuti, Proof Theory, North-Holland, Amsterdam, 2nd ed., 1987.
• [17] A. J. Wilkie and J. B. Paris, On the scheme of induction for bounded arithmetic formulas, Annals of Pure and Applied Logic, 35 (1987), pp. 261–302.