证明论笔记（第二章第二节）

· · 学习·文化课

超限归纳

本章后半段最重要的内容是证明 PA 的一致性。Gentzen 的思路是这样的：为 PA 中的每一个证明分配一个序数，当 Gentzen 简化 (reduce) 一个证明时这个序数一定会下降。Gentzen 证明，如果一个证明的结论为空列（矛盾）他就能无限简化下去，而根据超限归纳（良序性）这是不可能的。因此 PA 没有结论为矛盾的证明。所以，当然，首先我们先来学习一下超限归纳。

超限归纳的意思是，我们可以从

得到对于任意 \beta<\alpha 的序数都有 P(\beta)。其中 \alpha 是我们约定好的上限；比如皮亚诺算术中它就是 \omega，因此它是"不太超限"的归纳。

接受越远的超限归纳意味着我们的理论越强，从而可能证明比它更弱的理论的一致性。当然，由于序数本身（可怕的）证明论意义，接受太远的超限归纳可能导致无法预测的后果……为了证明 PA 的一致性，我们需要直到 \varepsilon_0 的超限归纳。所以先这样吧。

事实上即使在皮亚诺算术中我们也可以谈论（\varepsilon_0 以下）的序数：

于是，很显然，一个（小于 \varepsilon_0 的）序数可以用有限长的序数的列表表达；自然可以用皮亚诺算术表达，进而被哥德尔编码。

序数上自然可以定义序数和、序关系、序数积、自然数乘方等等，大家都很熟悉了所以不表。

应用以上定义（蕴含直到 \varepsilon_0 的超限归纳）已经足以证明 \varepsilon_0（指集合 \varepsilon_0；以上内容无法定义 \varepsilon_0 更没法证明不存在从 \varepsilon_0 本身出发的无穷递降链）的良序性，不需要任何的集合论公理（事实上我们这里定义的"序数"本身也没有集合论含义）。证明不表。

特别地，我们将记 \omega_1=\omega,\omega_2=\omega^{\omega},\omega_n=\omega^{\omega^{\ldots}}。

接下来进入正题。

Gentzen's Consistency Proof

引理.

定义.

PA 中的一个证明被称为是简单的当且仅当它

  • 没有自由变元
  • 只使用算术公理（不形如 A\rightarrow A，只使用皮亚诺中新加的公理）
  • 只使用结构性推理
  • 不使用本质的切割

无法简单地证明 \rightarrow。

证明.

**定义. (Gentzen 的序数指派)** 设 $S$ 是一个列，$P$ 是一个证明。 - 一个命题的**复杂度**是其所含的逻辑符号的数量；一个切割推理的复杂度是其切掉的命题的复杂度；一个归纳推理的复杂度是其归纳步骤 $F(a)$ 和 $F(a')$ 的复杂度。 - $h(S,P)$ 是 $S$ 在 $P$ 中的**高度**，等于其下方切割推理和归纳推理的复杂度的最大值。 下面正式开始定义 $o(S,P)$。 - 若 $S$ 是公理，那么 $o(S,P)=\omega^0$。 - 若 $S$ 由 $S'$ 通过非切割的结构性推理得到，$o(S,P)=o(S',P)$​。 - 若 $S$ 由 $S'$ 通过逻辑性推理得到，$o(S,P)=o(S',P)+1$。若 $S$ 由 $S',S''$ 通过逻辑性推理得到，$o(S,P)=o(S',P)\sharp o(S'',P)$。（其中 $\sharp$ 是自然和而不是序数和） - 若 $S$ 由 $S',S''$ 通过切割得到， $$ o(S,P)=\omega^{\omega^{\ldots^{(o(S',P)\sharp o(S'',P))}}} $$ 其中 $\omega$ 指数塔有"$S$ 和 $S',S''$ 高度的差"层。 - 若 $S$ 由 $S'$ 通过归纳得到，而且 $S'$ 的 Cantor 标准形中最高的一项为 $\omega^{\alpha_1}$，那么 $$ o(S,P)=\omega^{\omega^{\ldots^{\omega^{\alpha_1+1}}}} $$ 其中如果不算顶部的 $\omega^{\alpha_1+1}$，$\omega$ 指数塔有"$S$ 和 $S'$ 高度的差"层。 令 $o(P)$ 为结论 $S$ 的 $o(S,P)$。 有时候，为了方便，对于 $P$，我们会把它的 $o(P)$ 记在结论的 $\rightarrow$ 上，即 $$ P\dfrac{\ldots}{\Gamma\xrightarrow{o(P)}\Delta} $$

自然 o(P)<\varepsilon_0。我们只需要接受直到 \varepsilon_0 的超限归纳。

定理.

如果 P 是一个 \rightarrow 的证明，存在另一个证明 P'，o(P')<o(P)。

证明. (Gentzen's Consistency Proof)

下面我们开始化简 (reduction) P。

首先称，从结论（\rightarrow）往上回溯，直到遇到逻辑性推断（这些列不包含逻辑性推断的前提但包含结论）；所有这些列被称为证明的结尾。

步骤 1. 循环此步直到不能再进行。如果 P 的结尾中含有一个不作为归纳推断所用的变元的自由变元（结尾中不含逻辑性推断；而且由于正则性，它不在证明的其他地方作为 \forall,\exists 或归纳推断所用的变元出现），把它替换为 0。

步骤 1 不影响 o(P)。

步骤 2. 假设 P 的结尾中有至少一个归纳。选取其中最低的一个，形如

\dfrac{P_0\dfrac{\ldots}{F(a),\Gamma\xrightarrow{\mu}\Delta,F(a')}}{F(0),\Gamma\rightarrow\Delta,F(s)}

由于经过了步骤 1 而且该归纳推断最低，所以 s 无自由变元。自然存在唯一 \overline m，\rightarrow s=\overline m 可（不需要本质的切割和归纳地）证，进而 F(\overline m)\rightarrow F(s) 亦然。令 Q 是这样一个证明。

已知 \overline m，我们就可以"手动归纳"，具体来说可以得到如下证明：

\dfrac{P_0(\overline 0)\dfrac{\ldots}{F(0),\Gamma\xrightarrow{\mu}\Delta,F(0')}\qquad P_0(\overline 1)\dfrac{\ldots}{F(0'),\Gamma\xrightarrow{\mu}\Delta,F(0'')}}{F(0),\Gamma\rightarrow\Delta,F(0'')}

进而得到一个 F(0),\Gamma\rightarrow\Delta,F(\overline m) 的证明。配合上先前的 Q，我们就得到了一个替代品。

当然更关键的是分析这样的替代对 o(P) 的影响如何。注意到 F(\overline n),\Gamma\rightarrow\Delta,F(\overline{n+1}) 全都具有相同的高度，因此新证明的 o 是 m\mu 加上一个小于 \omega 的常数（即 o(Q)），相对于 \omega^{\alpha_1+1} 有着压倒性的优势。

步骤 2 只需进行一次就可以退出流程（已经得到了一个更小的 P'）。接下来，如果进入了步骤 3，那么我们便假设 P 的结尾中已经没有归纳。

步骤 3. 假设 P 中含有一个形如 D\rightarrow D 的公理，两个 D 都必须以切割消去。这部分证明有点像切割消除定理，所以我们仍会跳过。o(P) 的减小的证明基于不等式 \omega^{\alpha}\sharp\omega^{\beta}<\omega^{\alpha\sharp\beta}。

同样，如果进入步骤 4，那么我们便假设 P 的结尾中没有自由变元、归纳、逻辑推断和非算术公理。

步骤 4. 主要是为了步骤 5 准备。循环此步直到不能再进行。如果 P 的结尾中有一个弱化推断，则我们可以把它消除。具体细节根本就没人关心所以仍然跳过。

现在 P 的结尾中没有自由变元、归纳、弱化、逻辑推断和非算术公理。

步骤 5. 显然，由于本章最开头的引理，P 现在绝不可能是它自己的结尾。

如果对于一个切割推断来说，它所切掉的两个（相同的）命题，各自都是在结尾"边界"的推断中新引入的，那么称这个切割归纳是合适的。合适于什么呢，当然是合适于消去了。不过消去的论证先放一下，我们现在证明 P 中一定存在这样一个合适的切割归纳。

证明.

由于 P 不是自己的结尾，那么由边界的逻辑推断引入的含逻辑连接词的命题必定只能被切割律消去，因此 P 中一定有一个本质的切割。取其最低的一个，称为 I。如果 I 本身就是一个合适的切割那就证完了。否则令其形如

I\dfrac{P_1\dfrac{\ldots}{\Gamma\rightarrow\Delta,D}\quad P_2\dfrac{\ldots}{D,\Pi\rightarrow\Lambda}}{\Gamma,\Pi\rightarrow\Delta,\Lambda}

不妨假设 P_1 中的 D 并非由边界的逻辑推断引入。

现在取 $P_1$ 中的（对于 $P$ 的）一个边界推断 $J$。$J$ 当然也是 $P_1$ 的一个边界推断。因为 $J$ 的存在，$P_1$ 也不是自己的结尾。那么我们对 $P_1$ 归纳即可。

现在取得了合适的切割，我们取其最低一个，不妨令其形如

I\dfrac{\dfrac{\dfrac{J_1\dfrac{\Gamma'\rightarrow\Theta',A\quad \Gamma'\rightarrow\Theta',B}{\Gamma'\rightarrow\Theta',A\land B}}{\cdots}}{\Gamma\xrightarrow{\mu}\Theta,A\land B}\quad \dfrac{\dfrac{J_2\dfrac{A,\Pi'\rightarrow\Lambda'}{A\land B,\Pi'\rightarrow\Lambda'}}{\cdots}}{A\land B,\Pi\xrightarrow{\nu}\Lambda}}{\Gamma,\Pi\rightarrow\Theta,\Lambda}

注意这里我们令 D=A\land B 由 \land 推断引入。其他逻辑推断同理，不表。

下面我们重写这个证明；事实上我们将要表明，\Gamma'\rightarrow\Theta',B 那一支完全是不必要的。

我们从 I 向下，找到第一个和 I 的前提高度不同的列 \Delta\rightarrow\Xi。自然它是一个切割 K 的结论。注意 \Delta\rightarrow\Xi 可能就是 I 的结论本身也有可能是 \rightarrow。但它必定是存在的。

考虑如下证明

I_1'\dfrac{\dfrac{\dfrac{J_1'\dfrac{\Gamma'\rightarrow\Theta',A}{\Gamma'\rightarrow \Theta',A,A\land B}}{\cdots}}{\Gamma\xrightarrow{\mu'}\Theta,A,A\land B}\quad A\land B,\Pi\xrightarrow{\nu}\Lambda}{\Gamma,\Pi\rightarrow \Theta,\Lambda,A}

令 I'_1 通过和 I 类似的推理得到 \Delta\rightarrow\Xi, A。

和如下证明

I_2'\dfrac{\Gamma\xrightarrow{\mu}\Theta,A\land B\quad \dfrac{\dfrac{J_2'\dfrac{A,\Pi'\rightarrow\Lambda'}{A\land B,A,\Pi'\rightarrow \Lambda'}}{\cdots}}{A\land B,A,\Pi\xrightarrow{\nu'}\Lambda}}{A,\Gamma,\Pi\rightarrow \Theta,\Lambda}

令 I'_2 通过和 I 类似的推理得到 A,\Delta\rightarrow\Xi。接下来两者进行切割，得到完整证明。

综上，步骤 5 一定能进行而且一定使 $o(P)$ 减小。证毕。

合上超限归纳，我们得到

定理.

PA 一致。

可证良序

定义.

$$ \exists y(\overline f(x_1,\ldots,x_n,y)=0) $$ 其中 $\overline f$ 是一个原始递归函数的形式化版本。 $L$ 上的一个 $\Pi_1^0$ 命题形如下 $$ \forall y(\overline f(x_1,\ldots,x_n,y)=0) $$

可以证明，任何原始递归关系都可写成 \Sigma_1^0 或 \Pi_1^0 的形式。

定义. (可证良序)

我们在 PA 中加入一个一元常谓词 \varepsilon 和一个自然数上的原始递归良序关系 <\cdot。不妨设 <\cdot 中的最小元素为 0。由前 <\cdot 可以被写为一个 \Sigma_1^0 命题；对于后者我们仍采用 <\cdot 这个记号。

如果

\forall x(\forall y<\cdot x(\varepsilon(y)\supset\varepsilon(x)))\rightarrow\varepsilon(a)

（记为 TI(<\cdot)）

在 PA 中可证，那么称 <\cdot 是一个可证良序。

定理. (Gentzen)

如果 <\cdot 是一个可证良序，那么存在一个原始递归函数 f:\mathbb{N}\rightarrow\varepsilon_0（还记得我们可以在皮亚诺算术中讨论小于 \varepsilon_0 的序数）使得

  • 存在序数 \mu<\varepsilon_0，f(a)\prec\overline\mu。

或者你也可以用更炫酷的方法表达这个定理：PA 的证明论序数为 \varepsilon_0。

显然，正如我们做了很多次的那样，我们可以在 PA 中加入公理

\forall x(x<\cdot t\supset \varepsilon(x))\rightarrow\varepsilon(t)

称新系统为 TJ。<\cdot 是可证良序意味着形如 \rightarrow\varepsilon(\overline m_1),\ldots,\varepsilon(\overline m_n) 的结论在 TJ 中皆可证。令 m_i 中的最小者为 TJ 的终值；更具体一点，令 |m|_{<\cdot} 是所有 <\cdot\overline m 的元素构成的序型，令其（序数自然序）的最小者为 TJ 的终值。

我们的证明思路如下：我们构造一个魔改的 Gentzen Reduction。

这样，我们就可以证明终数总是不大于 o(P)。利用在 o 上的超限归纳：不关键的情况显然，对于关键的情况，如果终数大于 o(P)，应用新 Reduction 把终数修改为 o(P) 便由归纳得到矛盾。

假设我们已经对 P 做了步骤 1\~4，那么 P 现在满足如下性质：

  • 如果 P 中有一个弱化 I，那么 I 以下的所有推断都是弱化。（步骤 4 我们之前没详细讲，这里接受即可。）

这时，P 至少有一个逻辑推断或 TJ 的新公理（回忆上一章开头的引理）。因此 P 的结尾的边界上至少有一个逻辑推断或 TJ 的新公理。

如果 P 也通过了步骤 5，那么它只能是 TJ 新公理，形如

\forall x(x<\cdot t\supset \varepsilon(x))\rightarrow\varepsilon(t)

并且（通过一些痛苦的证明）最终会在结论中体现为 \varepsilon(\overline m_i)。取任意 m 使得 |m|_{<\cdot} 小于 P 的终数。那么 \rightarrow\overline m<\cdot t 是一个真的、\Sigma_1^0 的列，从而可以用一个公理和一次 \exists 推断直接证明。因此我们可以把上式替换为

\dfrac{\dfrac{\dfrac{\dfrac{\rightarrow F}{\rightarrow\overline m<\cdot r}\quad \varepsilon(\overline m)\rightarrow\varepsilon(\overline m)}{m<\cdot r\supset\varepsilon(\overline m)\rightarrow\varepsilon(\overline m)}}{\forall x(x<\cdot r\supset\varepsilon(\overline x))\rightarrow\varepsilon(\overline m)}}{\forall x(x<\cdot r\supset\varepsilon(\overline x))\rightarrow\varepsilon(\overline m),\varepsilon(r)}