（你可能会发现这期主题好像不一样，其实是因为公式太多 typora 崩了所以只能换 vscode 导出）

在这章中，我们（终于）将学会算术了。更具体来说是一阶皮亚诺算术。

皮亚诺算术的形式化

皮亚诺算术的逻辑语言中有以下内容：

• 常量 $0$$0$。

• 常函数 ${}^{\prime },+,\cdot$$',+,\cdot$。（其中 ${}^{\prime }$$'$ 为一元，$+,\cdot$$+,\cdot$ 为二元。）

• 常谓词 $=$$=$。

一个数是形如 $0^{″}{\dots }^{\prime }$$0''\ldots'$ 的表达式。我们记其为 $\bar{n}$$\overline n$。（如果没有强调的必要，我们一般还是直接记为 $n$$n$ 算了。）

皮亚诺算术的第一公理体系（称为 CA）中有如下内容：

• $\mathrm{\forall }x\mathrm{\forall }y(x^{\prime }=y^{\prime }\supset x=y)$$\forall x\forall y(x'=y'\supset x=y)$

• $\mathrm{\forall }x(\mathrm{\neg }{x}^{\prime }=0)$$\forall x(\neg x'=0)$

• $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(x=y\supset y=z\supset x=z)$$\forall x\forall y\forall z(x=y\supset y=z\supset x=z)$

• $\mathrm{\forall }x\mathrm{\forall }y(x=y\supset x^{\prime }=y^{\prime })$$\forall x\forall y(x=y\supset x'=y')$

• $\mathrm{\forall }x(x+0=x)$$\forall x(x+0=x)$

• $\mathrm{\forall }x\mathrm{\forall }y(x+y^{\prime }=(x+y{)}^{\prime })$$\forall x\forall y(x+y'=(x+y)')$

• $\mathrm{\forall }x(x\cdot 0=0)$$\forall x(x\cdot 0=0)$

• $\mathrm{\forall }x\mathrm{\forall }y(x\cdot y^{\prime }=x\cdot y+x)$$\forall x\forall y(x\cdot y'=x\cdot y +x)$

皮亚诺算术的第二公理体系（称为 VJ）中有如下内容：

• $\mathrm{\forall }{z}_1\dots \mathrm{\forall }{z}_n\mathrm{\forall }x(F(0,z)\wedge \mathrm{\forall }y(F(y,z)\supset F(y^{\prime },z))\supset F(x,z))$$\forall z_1\ldots\forall z_n\forall x(F(0,z)\land\forall y(F(y,z)\supset F(y',z))\supset F(x,z))$

请注意一阶皮亚诺（一如所有一阶逻辑语言一样）是没有谓词上的量词的，所以上述公理没有 $\mathrm{\forall }F$$\forall F$ 而是对每个谓词 $F$$F$ 单独开一条公理。但是这有什么区别呢？在很久以后我们才能了解这两种体系的区别是……多么恐怖。

（读者可以尝试一下证明加法交换律 $a+b=b+a$$a+b=b+a$。）

和其他公理体系一样，我们也可以通过另一种方法得到皮亚诺算术，具体来说我们可以通过

• 增加如下初始列：

• • $s^{\prime }=t^{\prime }\to s=t$$s'=t'\rightarrow s=t$

  • $s^{\prime }=0\to$$s'=0\rightarrow$

  • $s=t,t=r\to s=r$$s=t,t=r\rightarrow s=r$

  • $s=t\to s^{\prime }=t^{\prime }$$s=t\rightarrow s'=t'$

  • $\to s+0=s$$\rightarrow s+0=s$

  • $\to s+t^{\prime }=(s+t{)}^{\prime }$$\rightarrow s+t'=(s+t)'$

  • $\to s\cdot 0=0$$\rightarrow s\cdot 0=0$

  • $\to s\cdot t^{\prime }=s\cdot t+s$$\rightarrow s\cdot t'=s\cdot t+s$

• 并增加新的一种推断

来得到皮亚诺算术 PA。

定理.

一个列可以通过 $CA\cup VJ$$CA\cup VJ$（在 LK 中）证明当且仅当它可以在 PA 中被证明。

现在我们看看能不能把 LK 上的论断搬到 PA 上。

对于正则性和之前是一样的。

• （用与之前相同的方法）可以证明 PA 上的证明都可以被替换为它的正则版本。

现在我们来看看切割和归纳（在什么情况下）能去除。

• 对于任何没有自由变元的项 $s$$s$，总存在唯一一个数 $\bar{n}$$\overline n$，使得 $s=\bar{n}$$s=\overline n$ 的可证且不需要本质的切割和归纳。（本质的切割指切掉的命题不形如 $s=t$$s=t$ 的切割推理。见上一章的带等号的谓词推演一节。）

• • 由于加法和乘法的简单结构，在项上归纳即可。

• 令 $s,t$$s,t$ 皆为没有自由变元的项，要么 $\to s=t$$\rightarrow s=t$ 可证要么 $s=t\to$$s=t\rightarrow$ 可证，且不需要本质的切割和归纳。

• • 只需要注意到对于 ${\bar{n}}_1,{\bar{n}}_2$$\overline n_1,\overline n_2$，以上论断是显然的，然后应用上一个命题即可。

• 假设 $\to s=t$$\rightarrow s=t$ 可（不需要本质的切割和归纳地）证，那么令 $q(a),r(a)$$q(a),r(a)$ 是两个项，$q(s)=r(s)\to q(t)=r(t)$$q(s)=r(s)\rightarrow q(t)=r(t)$ 可证且不需要本质的切割和归纳。

• • 同理。

• 假设 $\to s=t$$\rightarrow s=t$ 可（不需要本质的切割和归纳地）证，那么对于任意命题 $F(a)$$F(a)$，$s=t,F(s)\to F(t)$$s=t,F(s)\rightarrow F(t)$ 可证，且不需要本质的切割和归纳。

• • 同理。

不完备性定理

很不幸的是，众所周知，PA 是不完备的。事实上，所有 PA 的扩展都是不完备的。具体来说

定义.

如果公理系统 $\mathcal{A}$$\mathscr A$ 恰好是一组（有限个）公理范式的所有实例，称 $\mathcal{A}$$\mathscr A$ 是可公理化的。如果某形式系统和 ${\mathsf{LK}}_{\mathcal{A}}$$\mathsf{LK}_{\mathscr A}$ 等价，那么称它也是可公理化的。

一个系统 $\mathbf{S}$$\mathbf S$ 被称为一个 PA 的扩展当且仅当所有 $\mathbf{PA}$$\mathbf {PA}$ 中的定理都能在 $\mathbf{S}$$\mathbf{S}$ 中证明。

本节我们主要研究那些可公理化的 PA 的扩展。

下面让我们进入 Gödel's Incompleteness Theorem 的证明。先让我们准备一些（主要在数论部分有用的）小工具。

定义.

以下归纳定义的函数被称为原始递归函数。

• $f(x_1)=x_1^{\prime }$$f(x_1)=x_1'$。

• $f(x)=k$$f(x)=k$​。（参数组 $x_1,x_2,\dots ,x_n$$x_1,x_2,\ldots,x_n$ 简记为 $x$$x$。）

• $f(x)=x_i$$f(x)=x_i$。

• $f(x)=g(h_1(x),\dots ,h_m(x))$$f(x)=g(h_1(x),\ldots,h_m(x))$，其中 $g,h$$g,h$ 都是原始递归函数。

• $f(0)=k,f(x_1^{\prime })=g(x_1,f(x_1))$$f(0)=k,f(x_1')=g(x_1,f(x_1))$，其中 $g$$g$ 是原始递归函数。

• $f(0,x)=g(x),f(x_1^{\prime },x)=h(x_1,f(x_1,x))$$f(0,x)=g(x),f(x_1',x)=h(x_1,f(x_1,x))$，其中 $g,h$$g,h$ 都是原始递归函数。

一个 $n$$n$ 元关系 $R$$R$ 被称为原始递归关系，当且仅当存在一个只取 $0,1$$0,1$ 的原始递归函数 $f(x)$$f(x)$ 使得 $R(x)$$R(x)$ 当且仅当 $f(x)=0$$f(x)=0$。

（请区别谓词和 $n$$n$ 元关系；回忆一个形式系统和它的模型。事实上我们也应该区别形式函数和函数，接下来用 $\bar{f}$$\overline f$ 表示形式化版本而 $f$$f$ 表示原始递归表述。）

例如，$+$$+$ 和 $\cdot$$\cdot$ 都是原始递归函数，$=$$=$ 和 $<$$<$ 都是原始递归关系。

定理.

原始递归函数可以用 PA 的逻辑语言表达，它们的定义都可以用 PA 证明。

称一个函数能被一个逻辑语言表达当且仅当存在一个命题 $\varphi$$\phi$ 使得

$$f(x)=y\leftrightarrow \varphi (x,y)$$

证明.

下面我们介绍 Gödel's β。

$$\beta (x_1,x_2,x_3)=x_{1}mod(1+x_2\cdot (x_3+1))$$

考虑到我们可以用 $\mathrm{\exists }$$\exists$ 之类的东西表达整除，所以在 PA 中是可以表达 $\beta$$\beta$ 的，但是想想都恶心所以我们这里还是不写了。

这个 $\beta$$\beta$ 函数有什么用呢？那是因为：

对于任意 $(k_0,k_1,\dots ,k_n)$$(k_0,k_1,\ldots,k_n)$，存在数 $b,c$$b,c$，

$$\beta (b,c,i)=k_i$$

（注意到我们可以令 $c=(n+1)!$$c=(n+1)!$ 使得模各自互质，$b$$b$ 就显然了。）

因此，$\beta$$\beta$ 函数可以完美起到构造函数的作用。

不妨举原始递归函数的第五条定义的例子，这时 $f(n)=m$$f(n)=m$ 等价于

$$\mathrm{\exists }b\mathrm{\exists }c\beta (b,c,0)=k\wedge \mathrm{\forall }i(i<n)\to (\beta (b,c,i^{\prime })=g(i,\beta (b,c,i))\wedge \beta (b,c,n)=m$$

这不仅完全使用了 PA 的语言，而且 PA 可证。

进而 $n$$n$ 元关系们自然亦然。

那么首先我们需要能够在命题中讨论命题和证明本身。我们需要介绍哥德尔编码。

定义. (Gödel's Numbering)

令每一个逻辑语言符号 $X$$X$（加上推理符号 $\to$$\rightarrow$ 和横线 $-$$-$）对应一个数 $\lceil X\rceil$$\lceil X\rceil$；

令列 $X_0{X}_1{X}_2\dots$$X_0X_1X_2\ldots$ 对应

$$2^{\lceil X_0\rceil }{3}^{\lceil X_1\rceil }{5}^{\lceil X_2\rceil }\dots$$

记为 $\lceil X_0{X}_1{X}_2\dots \rceil$$\lceil X_0X_1X_2\ldots\rceil$。

特别地令证明 $Q/S$$Q/S$ 对应

$$2^{\lceil Q\rceil }{3}^{\lceil -\rceil }{5}^{\lceil S\rceil }$$

引理.

• "替换"操作可以被算术化为一个原始递归函数。具体来说存在 $\text{sb}(\lceil X(a_0)\rceil ,\lceil Y\rceil )=\lceil X(Y)\rceil$$\text{sb}(\lceil X(a_0)\rceil,\lceil Y\rceil)=\lceil X(Y)\rceil$，其中 $a_0$$a_0$ 被完全指示。

• $\lceil \bar{m}\rceil$$\lceil \overline m\rceil$（即数 $m$$m$ 的形式化表达的哥德尔编码）可以被算术化为一个原始递归函数，记为 $v(m)$$v(m)$。

• "$P$$P$ 是 $S$$S$ 的证明"可以被算术化为一个原始递归关系。具体来说存在 $\text{Prov}(\lceil P\rceil ,\lceil S\rceil )$$\text{Prov}(\lceil P\rceil,\lceil S\rceil)$ 当且仅当 $P$$P$ 是 $S$$S$ 的证明。

这才是整个证明最难的地方吧喂。

我们很难指出具体的原始递归函数，但是有个绕了很大一圈以至于有点搞笑的证明方法：以上形式化操作显然都可以通过图灵机计算，因此根据丘奇-图灵论题它们也一定能被原始递归函数表达。

定理.

简记 $\mathrm{\exists }x\overline{\text{Prov}}(x,\overline{\lceil A\rceil })$$\exists x\overline{\text{Prov}}(x,\overline{\lceil A\rceil})$ 为 $\overline{\text{Pr}}(\overline{\lceil A\rceil })$$\overline{\text{Pr}}(\overline{\lceil A\rceil})$。（$\overline{\lceil A\rceil }$$\overline{\lceil A\rceil}$ 可能看着非常奇怪。毕竟 $\lceil A\rceil$$\lceil A\rceil$ 是一个数，上划线其实可以忽略。）

$$\overline{\text{Pr}}(\overline{\lceil A\rceil })\to \overline{\text{Pr}}(\overline{\lceil \stackrel{―}{\text{Pr}}(\stackrel{―}{\lceil A\rceil })}\rceil )$$

可证。

证明.

如果 $A$$A$ 可由 $P$$P$ 证，那么 $\text{Prov}(\lceil P\rceil ,\lceil A\rceil )$$\text{Prov}(\lceil P\rceil,\lceil A\rceil)$ 对应的原始递归函数恒为 $0$$0$。由于，我们知道，原始递归函数的点值皆可证，那么 $\text{Prov}(\lceil P\rceil ,\lceil A\rceil )$$\text{Prov}(\lceil P\rceil,\lceil A\rceil)$ 自然也是可证的。

（事实上以上推理对任何原始递归关系都成立：一个原始递归关系如果恒为真，那么它的形式化版本是可证的。）

万事具备，我们已经可以开始搞事情了。

定理. (Tarski's undefinability theorem)

一个单一自由变元的命题 $T$$T$ 被称为真值定义，当且仅当对于所有没有自由变元的命题 $A$$A$，

$$T(\overline{\lceil A\rceil })\leftrightarrow A$$

可证。

如果该形式系统一致，那么真值定义不存在。

或者你也可以用更炫酷的方法表达这个定理：算术真值不可算术定义。

证明.

下面这个方法称作 Gödel's trick。实际上也是一种对角线构造：你可以在停机问题等等诸多地方找到它。

假设真值定义存在，那么令

• $F(a_0):=\mathrm{\neg }T(\overline{\text{sb}}(a_0,\bar{v}(a_0)))$$F(a_0):=\neg T(\overline{\text{sb}}(a_0,\overline v(a_0)))$；

• $p:=\lceil F(a_0)\rceil$$p:=\lceil F(a_0)\rceil$ 是它的哥德尔编码；

• $A_T:=F(\bar{p})$$A_T:=F(\overline p)$。在真值上它等价于 $\mathrm{\neg }T(\overline{\text{sb}}(\bar{p},\bar{v}(\bar{p})))$$\neg T(\overline{\text{sb}}(\overline p,\overline v(\overline p)))$，当然它并不如此编码。

那么自然有 $\lceil A_T\rceil =\lceil F(\bar{p})\rceil =\text{sb}(\lceil F(a_0)\rceil ,\lceil \bar{p}\rceil )=\text{sb}(p,v(p))$$\lceil A_T\rceil=\lceil F(\overline p)\rceil=\text{sb}(\lceil F(a_0)\rceil,\lceil \overline p\rceil)=\text{sb}(p,v(p))$，于是我们惊奇地发现

$$A_T\leftrightarrow \mathrm{\neg }T(\overline{\lceil A_T\rceil })$$

矛盾。得证。

定理. (Gödel's first incompleteness theorem)

如果在形式系统 $S$$S$ 中，对于任意命题 $A(a_0)$$A(a_0)$，如果 $\mathrm{\neg }A(\bar{n})$$\neg A(\overline n)$ 对 $n=0,1,2,\dots$$n=0,1,2,\ldots$ 皆可证，那么 $\mathrm{\exists }xA(x)$$\exists xA(x)$ 不可证，那么就说 $S$$S$ 是 $\omega$$\omega$-一致的。（注意 $\omega$$\omega$-一致（显然）蕴含一致。）

如果 $S$$S$ 是 $\omega$$\omega$-一致的，那么 $S$$S$ 不完备。

证明.

继续使用 Gödel's trick。

我们暂时记 $F(\alpha )$$F(\alpha)$ 这样的记法：其中 $\alpha$$\alpha$ 是一个谓词，这样我们就可以用命题来替换它。你将会看到这样的记法是安全的；我们并不涉及这样的命题替换的原始递归函数之类的问题。（即，不涉及 $\text{sb}(F(\alpha ),A)$$\text{sb}(F(\alpha),A)$；对于已经完成替换的命题，求其编码等操作完全具有良定义。）（我靠我解释这么多干什么）

记

• $p:=\lceil F(\overline{\text{Pr}}(\overline{\text{sb}}(a_0,\bar{v}(a_0))))\rceil$$p:=\lceil F(\overline{\text{Pr}}(\overline{\text{sb}}(a_0,\overline v(a_0))))\rceil$

• $A_F:=F(\overline{\text{Pr}}(\overline{\text{sb}}(\bar{p},\bar{v}(\bar{p}))))$$A_F:=F(\overline{\text{Pr}}(\overline{\text{sb}}(\overline p,\overline v(\overline p))))$

再一次地，$\lceil A_F\rceil =\text{sb}(p,v(p))$$\lceil A_F\rceil=\text{sb}(p,v(p))$ 显然成立，因此它可证，进一步

$$A_F\leftrightarrow F(\overline{\text{Pr}}(\overline{\lceil A_F\rceil }))$$

（不仅成立）也可证。

事实上，

引理. (Diagonal lemma)

对于 $S$$S$ 中的任意（单自由变元）命题 $F(a_0)$$F(a_0)$，总存在一个（无自由变元）命题 $A_F$$A_F$，满足

$$A_F\leftrightarrow F(\overline{\lceil A_F\rceil })$$

可证。

令 $F(\alpha )=\mathrm{\neg }\alpha$$F(\alpha)=\neg \alpha$，那么

$$A_F\leftrightarrow \mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil A_F\rceil })$$

可证。

如果 $A_F$$A_F$ 可证，那么 $\overline{\text{Pr}}(\overline{\lceil A_F\rceil })$$\overline{\text{Pr}}(\overline{\lceil A_F\rceil})$ 也可证（上上个定理），由于 $S$$S$ 一致，$\mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil A_F\rceil })$$\neg\overline{\text{Pr}}(\overline{\lceil A_F\rceil})$ 就不可证了，与 $A_F$$A_F$ 可证（并由上式立即给出一个 $\mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil A_F\rceil })$$\neg\overline{\text{Pr}}(\overline{\lceil A_F\rceil})$ 的证明）矛盾。因此 $A_F$$A_F$ 不可证。

（请注意反证法的是用 $\mathrm{\neg }$$\neg$ 推理等表达的，不涉及真值和语义问题。）

（这里我们只是懒得写推理步骤，如果你真的好奇的话可以看看接下来的 Gödel's second incompleteness theorem 的证明，那里我们写全了。）

下面说明 $\mathrm{\neg }{A}_F$$\neg A_F$ 也不可证。由于 $A_F$$A_F$ 不可证，那么 $\mathrm{\neg }\overline{\text{Prov}}(\bar{n},\overline{\lceil A_F\rceil })$$\neg\overline{\text{Prov}}(\overline n,\overline{\lceil A_F\rceil})$ 都成立，也就都可证，那么由 $\omega$$\omega$-一致，$\overline{\text{Pr}}(\overline{\lceil A_F\rceil })$$\overline{\text{Pr}}(\overline{\lceil A_F\rceil})$ 不可证，因此 $\mathrm{\neg }{A}_F$$\neg A_F$ 也不能可证（否则由上式立即给出一个 $\overline{\text{Pr}}(\overline{\lceil A_F\rceil })$$\overline{\text{Pr}}(\overline{\lceil A_F\rceil})$ 的证明）。

因此，$S$$S$ 不完备。

尽管 $A_F$$A_F$ 无法在 $S$$S$ 内被证明，但是"直觉上"它是真的，但这样的推理无法在 $S$$S$ 内表达。

你会想，嗯？为什么不能在 $S$$S$ 内表达？明明只要根据 $S$$S$ 一致我们就有——

定理. (Gödel's second incompleteness theorem)

如果 $S$$S$ 一致，$S$$S$ 的一致性在 $S$$S$ 中不可证。

更具体来说，令 ${\overline{\text{Consis}}}_S=\mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil 0=1\rceil })$$\overline{\text{Consis}}_S=\neg\overline{\text{Pr}}(\overline{\lceil 0=1\rceil})$。$A_F\leftrightarrow {\overline{\text{Consis}}}_S$$A_F\leftrightarrow\overline{\text{Consis}}_S$ 可证。而 $A_F$$A_F$ 不可证，因此一致性也不可证。

寄。

证明.

• 由于 ex falso quodlibet，$\mathrm{\neg }{\overline{\text{Consis}}}_S\leftrightarrow \mathrm{\forall }\lceil A\rceil \overline{\text{Pr}}(\overline{\lceil A\rceil })$$\neg\overline{\text{Consis}}_S\leftrightarrow\forall\lceil A\rceil\overline{\text{Pr}}(\overline{\lceil A\rceil})$ 可证。那么 $A_F\to \mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil A_F\rceil })\to {\overline{\text{Consis}}}_S$$A_F\rightarrow\neg\overline{\text{Pr}}(\overline{\lceil A_F\rceil})\rightarrow\overline{\text{Consis}}_S$。

• 显然 ${\overline{\text{Consis}}}_S,\overline{\text{Pr}}(\overline{\lceil A_F\rceil })\to \mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil \mathrm{\neg }{A}_F\rceil })$$\overline{\text{Consis}}_S,\overline{\text{Pr}}(\overline{\lceil A_F\rceil})\rightarrow \neg\overline{\text{Pr}}(\overline{\lceil \neg A_F\rceil})$，后者又等价于 $\mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil \stackrel{―}{\text{Pr}}(\stackrel{―}{\lceil A_F\rceil })\rceil })$$\neg\overline{\text{Pr}}(\overline{\lceil\overline{\text{Pr}}(\overline{\lceil A_F\rceil})\rceil})$。而我们早就知道 $\overline{\text{Pr}}(\overline{\lceil A_F\rceil })\to \overline{\text{Pr}}(\overline{\lceil \stackrel{―}{\text{Pr}}(\stackrel{―}{\lceil A_F\rceil })\rceil })$$\overline{\text{Pr}}(\overline{\lceil A_F\rceil})\rightarrow \overline{\text{Pr}}(\overline{\lceil\overline{\text{Pr}}(\overline{\lceil A_F\rceil})\rceil})$，因此

$${\overline{\text{Consis}}}_S,\overline{\text{Pr}}(\overline{\lceil A_F\rceil })\to \mathrm{\neg }{\overline{\text{Consis}}}_S$$

用一次 $\mathrm{\neg }$$\neg$ 推理和一次压缩即可得到

$${\overline{\text{Consis}}}_S\to \mathrm{\neg }\overline{\text{Pr}}(\overline{\lceil A_F\rceil })\to A_F$$

得证。

事实上，我们还可以把 Gödel's first incompleteness theorem 中的 $\omega$$\omega$-一致弱化（在结论上是强化）到一致。

证明. (Rosser)

令 $e$$e$ 是一个满足 $e(\lceil A\rceil )=\lceil \mathrm{\neg }A\rceil$$e(\lceil A\rceil)=\lceil \neg A\rceil$ 的原始递归函数。

令 $F(a_0):=$$F(a_0):=$

$$\mathrm{\exists }{x}_1(\overline{\text{Prov}}(x_1,a_0)\wedge \mathrm{\neg }\mathrm{\exists }{x}_2(x_2\le x_1\wedge \overline{\text{Prov}}(x_2,\bar{e}(a_0))))$$

即，"存在一个 $A$$A$ 的证明且不存在一个比它更（哥德尔编码意义上）小的 $\mathrm{\neg }A$$\neg A$ 的证明"。

你可能会疑惑这玩意听起来和 Gödel's first incompleteness theorem 的构造好像没啥区别。

由于 $S$$S$ 一致，所以 $\overline{\text{Prov}}(x_1,a_0)\to \mathrm{\neg }\overline{\text{Pr}}(\bar{e}(a_0))$$\overline{\text{Prov}}(x_1,a_0)\rightarrow\neg\overline{\text{Pr}}(\overline e(a_0))$。即 $\overline{\text{Pr}}(a_0)\to F(a_0)$$\overline{\text{Pr}}(a_0)\rightarrow F(a_0)$。且显然 $F(a_0)\to \overline{\text{Pr}}(a_0)$$F(a_0)\rightarrow\overline{\text{Pr}}(a_0)$，即 $F(a_0)\leftrightarrow \overline{\text{Pr}}(a_0)$$F(a_0)\leftrightarrow\overline{\text{Pr}}(a_0)$。

关键在于，利用 $S$$S$ 的一致性（并不在 $S$$S$ 中），我们才能证明这二者等价；在 $S$$S$ 中这是不可证的。

如果 $\overline{\text{Prov}}(x_1,a_0)\wedge \mathrm{\neg }\mathrm{\exists }{x}_2(x_2\le x_1\wedge \overline{\text{Prov}}(x_2,\bar{e}(a_0)))$$\overline{\text{Prov}}(x_1,a_0)\land \neg \exists x_2(x_2\le x_1\land \overline{\text{Prov}}(x_2,\overline e(a_0)))$ 成立，那么它一定是可证的：因为我们可以单纯地遍历所有 $x_2\le x_1$$x_2\le x_1$ 检验 $\overline{\text{Prov}}(x_2,\bar{e}(a_0))$$\overline{\text{Prov}}(x_2,\overline e(a_0))$。进而 $F(a_0)$$F(a_0)$ 也可证。

这里我们直接不作构造而是直接应用 Diagonal lemma 的结论，得到一个命题 $A_F$$A_F$ 满足

$$A_F\leftrightarrow \mathrm{\neg }F(\overline{\lceil A_F\rceil })$$

可证。

如果 $A_F$$A_F$ 可由证明 $P$$P$ 证明，那么由上式 $\mathrm{\neg }F(\overline{\lceil A_F\rceil })$$\neg F(\overline{\lceil A_F\rceil})$ 可证。由于已知 $A_F$$A_F$ 可证，所以一定存在一个比 $P$$P$ 更小的 $\mathrm{\neg }{A}_F$$\neg A_F$ 的证明，$S$$S$ 不一致。

如果 $\mathrm{\neg }{A}_F$$\neg A_F$ 可由证明 $P$$P$ 证明，那么由前面的论述 $F(\overline{\lceil \mathrm{\neg }{A}_F\rceil })$$F(\overline{\lceil\neg A_F\rceil})$ 可证（注意和 Gödel's first incompleteness theorem 的区别在这里显现了）。也就证明了不存在比 $P$$P$ 更小的 $A_F$$A_F$ 的证明，自然给出 $\mathrm{\neg }F(\overline{\lceil A_F\rceil })$$\neg F(\overline{\lceil A_F\rceil})$ 的证明，进而 $A_F$$A_F$ 可证，$S$$S$ 不一致。

超限归纳

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

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

• $P(0)$$P(0)$

• 如果任意小于 $\alpha$$\alpha$ 的序数 $\beta$$\beta$ 都满足 $P(\beta )$$P(\beta)$，那么 $P(\alpha )$$P(\alpha)$

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

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

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

• $0$$0$ 是序数。

• 如果 ${\mu }_i$$\mu_i$ 是序数，那么 ${\omega }^{{\mu }_1}+{\omega }^{{\mu }_2}+\dots +{\omega }^{{\mu }_k}$$\omega^{\mu_1}+\omega^{\mu_2}+\ldots+\omega^{\mu_k}$（这种表示方法称为 Cantor 标准形）也是序数。（其中 $k$$k$ 是（自然）数。）

• 只有通过以上两条得到的是序数。

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

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

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

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

接下来进入正题。

Gentzen's Consistency Proof

引理.

定义.

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

• 没有自由变元

• 只使用算术公理（不形如 $A\to A$$A\rightarrow A$，只使用皮亚诺中新加的公理）

• 只使用结构性推理

• 不使用本质的切割

无法简单地证明 $\to$$\rightarrow$。

证明.

$P$$P$ 中的所有命题都形如 $s=t$$s=t$，其中 $s,t$$s,t$ 都是没有自由变元的项，因此可以被简单地赋予"真值"。结构性推理和非本质切割的保"真值"性是显然的。

定义. (Gentzen 的序数指派)

设 $S$$S$ 是一个列，$P$$P$ 是一个证明。

• 一个命题的复杂度是其所含的逻辑符号的数量；一个切割推理的复杂度是其切掉的命题的复杂度；一个归纳推理的复杂度是其归纳步骤 $F(a)$$F(a)$ 和 $F(a^{\prime })$$F(a')$ 的复杂度。

• $h(S,P)$$h(S,P)$ 是 $S$$S$ 在 $P$$P$ 中的高度，等于其下方切割推理和归纳推理的复杂度的最大值。

下面正式开始定义 $o(S,P)$$o(S,P)$。

• 若 $S$$S$ 是公理，那么 $o(S,P)={\omega }^0$$o(S,P)=\omega^0$。

• 若 $S$$S$ 由 $S^{\prime }$$S'$ 通过非切割的结构性推理得到，$o(S,P)=o(S^{\prime },P)$$o(S,P)=o(S',P)$​。

• 若 $S$$S$ 由 $S^{\prime }$$S'$ 通过逻辑性推理得到，$o(S,P)=o(S^{\prime },P)+1$$o(S,P)=o(S',P)+1$。若 $S$$S$ 由 $S^{\prime },S^{″}$$S',S''$ 通过逻辑性推理得到，$o(S,P)=o(S^{\prime },P)\mathrm{♯}o(S^{″},P)$$o(S,P)=o(S',P)\sharp o(S'',P)$。（其中 $\mathrm{♯}$$\sharp$ 是自然和而不是序数和）

• 若 $S$$S$ 由 $S^{\prime },S^{″}$$S',S''$ 通过切割得到，

$$o(S,P)={\omega }^{{\omega }^{{\dots }^{(o(S^{\prime },P)\mathrm{♯}o(S^{″},P))}}}$$

其中 $\omega$$\omega$ 指数塔有"$S$$S$ 和 $S^{\prime },S^{″}$$S',S''$ 高度的差"层。

• 若 $S$$S$ 由 $S^{\prime }$$S'$ 通过归纳得到，而且 $S^{\prime }$$S'$ 的 Cantor 标准形中最高的一项为 ${\omega }^{{\alpha }_1}$$\omega^{\alpha_1}$，那么

$$o(S,P)={\omega }^{{\omega }^{{\dots }^{{\omega }^{{\alpha }_1+1}}}}$$

其中如果不算顶部的 ${\omega }^{{\alpha }_1+1}$$\omega^{\alpha_1+1}$，$\omega$$\omega$ 指数塔有"$S$$S$ 和 $S^{\prime }$$S'$ 高度的差"层。

令 $o(P)$$o(P)$ 为结论 $S$$S$ 的 $o(S,P)$$o(S,P)$。

有时候，为了方便，对于 $P$$P$，我们会把它的 $o(P)$$o(P)$ 记在结论的 $\to$$\rightarrow$ 上，即

$$P{\displaystyle \frac{\dots }{\mathrm{\Gamma }\stackrel{o(P)}{\to }\mathrm{\Delta }}}$$

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

定理.

如果 $P$$P$ 是一个 $\to$$\rightarrow$ 的证明，存在另一个证明 $P^{\prime }$$P'$，$o(P^{\prime })<o(P)$$o(P')<o(P)$。

证明. (Gentzen's Consistency Proof)

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

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

---

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

步骤 1 不影响 $o(P)$$o(P)$。

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

$${\displaystyle \frac{P_0{\displaystyle \frac{\dots }{F(a),\mathrm{\Gamma }\stackrel{\mu }{\to }\mathrm{\Delta },F(a^{\prime })}}}{F(0),\mathrm{\Gamma }\to \mathrm{\Delta },F(s)}}$$

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

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

$${\displaystyle \frac{P_0(\bar{0}){\displaystyle \frac{\dots }{F(0),\mathrm{\Gamma }\stackrel{\mu }{\to }\mathrm{\Delta },F(0^{\prime })}}{P}_0(\bar{1}){\displaystyle \frac{\dots }{F(0^{\prime }),\mathrm{\Gamma }\stackrel{\mu }{\to }\mathrm{\Delta },F(0^{″})}}}{F(0),\mathrm{\Gamma }\to \mathrm{\Delta },F(0^{″})}}$$

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

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

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

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

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

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

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

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

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

证明.

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

$$I{\displaystyle \frac{P_1{\displaystyle \frac{\dots }{\mathrm{\Gamma }\to \mathrm{\Delta },D}}{P}_2{\displaystyle \frac{\dots }{D,\mathrm{\Pi }\to \mathrm{\Lambda }}}}{\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Delta },\mathrm{\Lambda }}}$$

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

$P_1$$P_1$ 一定含有一个边界推断；否则 $D$$D$ 只能由公理引入，但是非算术公理已经在步骤 3 消除了，而算术公理又会导致 $I$$I$ 非本质，都矛盾。

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

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

$$I{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{J_1{\displaystyle \frac{{\mathrm{\Gamma }}^{\prime }\to {\mathrm{\Theta }}^{\prime },A{\mathrm{\Gamma }}^{\prime }\to {\mathrm{\Theta }}^{\prime },B}{{\mathrm{\Gamma }}^{\prime }\to {\mathrm{\Theta }}^{\prime },A\wedge B}}}{\cdots }}}{\mathrm{\Gamma }\stackrel{\mu }{\to }\mathrm{\Theta },A\wedge B}}{\displaystyle \frac{{\displaystyle \frac{J_2{\displaystyle \frac{A,{\mathrm{\Pi }}^{\prime }\to {\mathrm{\Lambda }}^{\prime }}{A\wedge B,{\mathrm{\Pi }}^{\prime }\to {\mathrm{\Lambda }}^{\prime }}}}{\cdots }}}{A\wedge B,\mathrm{\Pi }\stackrel{\nu }{\to }\mathrm{\Lambda }}}}{\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Theta },\mathrm{\Lambda }}}$$

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

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

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

考虑如下证明

$$I_1^{\prime }{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{J_1^{\prime }{\displaystyle \frac{{\mathrm{\Gamma }}^{\prime }\to {\mathrm{\Theta }}^{\prime },A}{{\mathrm{\Gamma }}^{\prime }\to {\mathrm{\Theta }}^{\prime },A,A\wedge B}}}{\cdots }}}{\mathrm{\Gamma }\stackrel{{\mu }^{\prime }}{\to }\mathrm{\Theta },A,A\wedge B}}A\wedge B,\mathrm{\Pi }\stackrel{\nu }{\to }\mathrm{\Lambda }}{\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Theta },\mathrm{\Lambda },A}}$$

令 $I_1^{\prime }$$I'_1$ 通过和 $I$$I$ 类似的推理得到 $\mathrm{\Delta }\to \mathrm{\Xi },A$$\Delta\rightarrow\Xi, A$。

和如下证明

$$I_2^{\prime }{\displaystyle \frac{\mathrm{\Gamma }\stackrel{\mu }{\to }\mathrm{\Theta },A\wedge B{\displaystyle \frac{{\displaystyle \frac{J_2^{\prime }{\displaystyle \frac{A,{\mathrm{\Pi }}^{\prime }\to {\mathrm{\Lambda }}^{\prime }}{A\wedge B,A,{\mathrm{\Pi }}^{\prime }\to {\mathrm{\Lambda }}^{\prime }}}}{\cdots }}}{A\wedge B,A,\mathrm{\Pi }\stackrel{{\nu }^{\prime }}{\to }\mathrm{\Lambda }}}}{A,\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Theta },\mathrm{\Lambda }}}$$

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

$h(\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Theta },\mathrm{\Lambda },A)=h(A,\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Theta },\mathrm{\Lambda })$$h(\Gamma,\Pi\rightarrow\Theta,\Lambda,A)=h(A,\Gamma,\Pi\rightarrow\Theta,\Lambda)$ 显然 $=h(\mathrm{\Delta }\to \mathrm{\Xi },A)=h(A,\mathrm{\Delta }\to \mathrm{\Xi })$$=h(\Delta\rightarrow\Xi, A)=h(A,\Delta\rightarrow\Xi)$（中间没有切割），也就 $=max(\text{complexity of }A,h(\mathrm{\Delta }\to \mathrm{\Xi }))$$=\max(\text{complexity of }A,h(\Delta\rightarrow\Xi))$。不论如何，总严格小于 $A\wedge B$$A\land B$ 的复杂度。剩下的序数不等式没人关心，不表。

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

合上超限归纳，我们得到

定理.

PA 一致。

可证良序

定义.

$L$$L$ 上的一个 ${\mathrm{\Sigma }}_1^0$$\Sigma_1^0$ 命题形如下

$$\mathrm{\exists }y(\bar{f}(x_1,\dots ,x_n,y)=0)$$

其中 $\bar{f}$$\overline f$ 是一个原始递归函数的形式化版本。

$L$$L$ 上的一个 ${\mathrm{\Pi }}_1^0$$\Pi_1^0$ 命题形如下

$$\mathrm{\forall }y(\bar{f}(x_1,\dots ,x_n,y)=0)$$

可以证明，任何原始递归关系都可写成 ${\mathrm{\Sigma }}_1^0$$\Sigma_1^0$ 或 ${\mathrm{\Pi }}_1^0$$\Pi_1^0$ 的形式。

定义. (可证良序)

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

如果

$$\mathrm{\forall }x(\mathrm{\forall }y<\cdot x(\epsilon (y)\supset \epsilon (x)))\to \epsilon (a)$$

（记为 $TI(<\cdot )$$TI(<\cdot)$）

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

定理. (Gentzen)

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

• $a<\cdot b$$a<\cdot b$ 当且仅当 $f(a)\prec f(b)$$f(a)\prec f(b)$；（后者是 ${\epsilon }_0$$\varepsilon_0$ 的自然序）

• 存在序数 $\mu <{\epsilon }_0$$\mu<\varepsilon_0$，$f(a)\prec \bar{\mu }$$f(a)\prec\overline\mu$。

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

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

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

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

• 如果一个 TJ 中的证明 $P$$P$ 能被我们先前定义的 Gentzen Reduction 的步减小 $o(P)$$o(P)$，那么称 $P$$P$ 不关键。否则当然就是关键的。

• 对于不关键的 $P$$P$，我们可以把它变为 $o(P)$$o(P)$ 更小，但终数不变的证明；（照抄 Gentzen Reduction）

• 对于关键的 $P$$P$，我们可以，呃……修改结论！把它变为 $o(P)$$o(P)$ 更小且终数为任意小于原终数的序数的证明。

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

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

• $P$$P$ 的结尾不含自由变元。

• $P$$P$ 的结尾不含归纳。

• $P$$P$ 的结尾不含逻辑性公理。

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

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

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

$$\mathrm{\forall }x(x<\cdot t\supset \epsilon (x))\to \epsilon (t)$$

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

$${\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\to F}{\to \bar{m}<\cdot r}}\epsilon (\bar{m})\to \epsilon (\bar{m})}{m<\cdot r\supset \epsilon (\bar{m})\to \epsilon (\bar{m})}}}{\mathrm{\forall }x(x<\cdot r\supset \epsilon (\bar{x}))\to \epsilon (\bar{m})}}}{\mathrm{\forall }x(x<\cdot r\supset \epsilon (\bar{x}))\to \epsilon (\bar{m}),\epsilon (r)}}$$

$o$$o$ 为 $6$$6$。因此，很简单，我们只需要给 TJ 的初始列指派复杂度为 $7$$7$ 即可。