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

· · 学习·文化课

来点轻松愉快的内容！（？）

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

皮亚诺算术的形式化

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

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

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

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

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

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

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

\dfrac{F(a),\Gamma\rightarrow\Delta,F(a')}{F(0),\Gamma\rightarrow\Delta,F(s)}

来得到皮亚诺算术 \mathbf{PA}。

定理.

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

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

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

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

不完备性定理

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

定义.

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

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

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

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

定义.

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

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

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

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

定理.

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

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

f(x)=y\leftrightarrow\phi(x,y)

证明.

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

\beta(x_1,x_2,x_3)=x_1\bmod(1+x_2\cdot (x_3+1))

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

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

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

\beta(b,c,i)=k_i

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

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

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

\exists b\exists c\quad\beta(b,c,0)=k\land \forall i\ (i<n)\rightarrow (\beta(b,c,i')=g(i,\beta(b,c,i))\land \beta(b,c,n)=m

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

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

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

定义. (Gödel's Numbering)

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

令列 X_0X_1X_2\ldots 对应

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

记为 \lceil X_0X_1X_2\ldots\rceil。

特别地令证明 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，其中 a_0 被完全指示。
  • "P 是 S 的证明"可以被算术化为一个原始递归关系。具体来说存在 \text{Prov}(\lceil P\rceil,\lceil S\rceil) 当且仅当 P 是 S 的证明。

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

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

定理.

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

\overline{\text{Pr}}(\overline{\lceil A\rceil})\rightarrow\overline{\text{Pr}}(\overline{\lceil \overline{\text{Pr}}(\overline{\lceil A\rceil})}\rceil)

可证。

证明.

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

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

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

定理. (Tarski's undefinability theorem)

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

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

可证。

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

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

证明.

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

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

那么自然有 \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 \neg T(\overline{\lceil A_T\rceil})

矛盾。得证。

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

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

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

证明.

继续使用 Gödel's trick。

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

记

  • 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}}(\overline p,\overline v(\overline p))))

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

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

（不仅成立）也可证。

令 F(\alpha)=\neg \alpha，那么

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

可证。

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

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

因此，S 不完备。

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

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

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

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

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

寄。

证明.

  • 由于 ex falso quodlibet，\neg\overline{\text{Consis}}_S\leftrightarrow\forall\lceil A\rceil\overline{\text{Pr}}(\overline{\lceil A\rceil}) 可证。那么 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})\rightarrow \neg\overline{\text{Pr}}(\overline{\lceil \neg A_F\rceil})，后者又等价于 \neg\overline{\text{Pr}}(\overline{\lceil\overline{\text{Pr}}(\overline{\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})\rightarrow \neg \overline{\text{Consis}}_S

用一次 \neg 推理和一次压缩即可得到

\overline{\text{Consis}}_S\rightarrow\neg\overline{\text{Pr}}(\overline{\lceil A_F\rceil})\rightarrow A_F

得证。