皮亚诺公理、形式系统和元数学——《数学女孩3：哥德尔不完备定理》笔记

2023.9.30 编：毕导出了一期视频讲解哥德尔不完备（第一、第二）定理，还蛮不错的，推荐观看。这里是链接：https://www.bilibili.com/video/BV19u4y1D7GT

# 元数学是什么

元数学就是研究数学的数学。

皮亚诺公理和形式系统都是在定义数学的微缩模型：

皮亚诺公理 (opens new window)定义了自然数和加法运算。
形式系统 (opens new window)则定义了一个更加根本的数学世界，它连真、假都没有，但却定义了命题、公理、证明、定理。

# 皮亚诺公理

皮亚诺公理定义了自然数的一般形式。

皮亚诺的这五条公理用非形式化的方法叙述如下：

$0$ 是自然数；
每一个确定的自然数 $a$ ，都有一个确定的后继数 $a'$ ， $a'$ 也是自然数；
对于每个自然数 $b$ 、 $c$ ， $b=c$ 当且仅当 $b'=c'$ ；
$0$ 不是任何自然数的后继数；
任意关于自然数的命题，如果证明：它对自然数 $0$ 是真的，且假定它对自然数 $a$ 为真时，可以证明对 $a'$ 也真。那么，命题对所有自然数都真。

皮亚诺公理 1-4 构建了一条自然数链，这条链由“后继”链接而成。四条公理分别保证了以下性质：

公理 1 保证存在一个自然数 $0$ ；
公理 2 保证每个自然数后面有且只有一个自然数；（链不会出现分叉，且保证自然数链无限长）
公理 3 保证每个自然数前面有且只有一个自然数；（链不会出现会合）
公理 4 保证 $0$ 是自然数链的首个自然数。

公理 5 保证了数学归纳法的正确性，因此我们可以在任何自然数相关的命题的证明中使用数学归纳法。

P. S. 皮亚诺公理除了可以定义 0、1、2 这样的自然数序列以外，还可以定义函数序列。定义出的函数序列如果具有以上性质，很多关于自然数的性质都可以直接搬到这个函数序列上。这便是邱奇数 (opens new window)，λ 演算中的自然数。

# 等于和等价关系

等价关系 (opens new window)是等于的一般形式。

满足以下三条性质的关系，可以被称为等价关系：

自反律： $a \sim a$
对称律： $a \sim b \Rightarrow b \sim a$
传递律： $a \sim b \wedge b \sim c \Rightarrow a \sim c$

除了“等于”以外，另一个常见的等价关系是“同模”：

1 \equiv 3 \pmod 2

# 形式系统

形式系统创造了一个更加根本的数学世界，并严格定义了命题、公理、证明、定理等概念。数学世界和形式系统中的概念对应关系如下：

数学	形式系统
命题	逻辑公式
公理	形式公理
证明	形式证明
定理	形式定理

P. S. 下文专注于讨论形式系统，故形式公理、形式证明和形式定理会被简写为公理、证明和定理。

# 定义一个形式系统

《数学女孩 3：哥德尔不完备定理》带我们从 0 开始，创造一个名为 $H$ 的形式系统（Formal system）。

# 逻辑公式 Well-Formed Formula

下面四条定义了形式系统 $H$ 中的逻辑公式：

F1：若 $x$ 是变量，则 $x$ 是逻辑公式
F2：若 $x$ 是逻辑公式，则 $\neg(x)$ 也是逻辑公式
F3：若 $x$ 和 $y$ 是逻辑公式，则 $(x)\vee(y)$ 也是逻辑公式
F4：只有上面三条规定的内容是逻辑公式

我们规定大写字母表示变量。例如 $A$ 是变量，则 $A$ 也是逻辑公式。

注意， $x \vee y$ 不是逻辑公式：需要逐字符匹配上面的定义，F3 是带有括号的。

顺便补充一下语句的定义：语句是没有自由变量的逻辑公式。

在上面四个逻辑公式的基础上，我们补充一个省略形式 $\rightarrow$ ：

IMPLY：把 $(x)\rightarrow(y)$ 定义为 $(\neg(x))\vee(y)$

# 形式公理 Axiom

形式系统中的公理，不是指必定为真（形式系统中甚至没有真假）的逻辑公式，而是能在证明时无条件使用的逻辑公式。

形式系统里没有讨论真假，而是在关注证明。

形式系统 $H$ 中的公理是以下四条中任意形式的逻辑公式：

P1： $((x)\vee(x)) \rightarrow x$
P2： $(x) \rightarrow ((x)\vee(y))$
P3： $((x)\vee(y)) \rightarrow ((y)\vee(x))$
P4： $((x)\rightarrow(y)) \rightarrow (((z)\vee(x)) \rightarrow ((z)\vee(y)))$

再次强调，上面四条公理在证明时可以直接使用。

# 推理规则 Inference Rule

推理规则 MP：根据 $x$ 和 $(x)\rightarrow(y)$ 可推出 $y$

# 形式证明和形式定理 Formal Proof & Theorem

通过定义了逻辑公式、公理、推理规则，我们就可以以形式的方式，定义什么是证明了。

我们基于公理、进行推理、构成证明——这是数学中重要的一环。

在形式系统 $H$ 中，我们把以下逻辑公式的有限序列称为逻辑公式 $a_n$ 的证明：

a_1, a_2, a_3, ..., a_k, ..., a_n

对于所有的 $a_k (1 \leq k \leq n)$ ，下面的 (1) 或 (2) 成立：

(1) $a_k$ 是公理；
(2) 存在小于 $k$ 的自然数 $s$ 、 $t$ ，根据 $a_s$ 和 $a_t$ 可推出 $a_k$ 。（注意，这句话是推理规则 MP）

此外， $a_n$ 这个逻辑公式，也可以被称为定理。

这样一来，我们就定义了逻辑公式、公理、推理规则、证明，以及定理。没有出现实数，也没有出现直线，更没有二次函数、方程、矩阵。我们只是在形式上建立了数学最为基础的部分。

# 习题：(A)->(A) 是形式定理吗

如果按照式子的含义来看的话，很显然是成立的。但我们在讨论形式系统，请不要关注式子的含义，而是完全关注式子的形式。

泰朵拉：原来一边听还一边不能被含义牵着走是这么难啊。
米尔嘉：习惯问题。只要能降低自己的体温（像计算机一样冰冷地思考）就行。当然，人类是不可能不思考含义的。而且，这种形式系统也不是胡乱生成出来的。其背后肯定有目的——生成这种有意思的系统的目的。重要的是，不能由人来进行思考，而要从形式上、机械性地进行思考。

这里的思路是基于 P4：

((x)\rightarrow(y)) \rightarrow (((z)\vee(x)) \rightarrow ((z)\vee(y)))

思路是，将求证的式子变换为 $(z)\vee(y)$ ，然后分别证明 $(x)\rightarrow(y)$ 和 $(z)\vee(x)$ ，即可使用两次 MP 完成证明。

第一步，首先将需要证明的 $(A)\rightarrow(A)$ 改写为 $(\neg(A))\vee(A)$ ，这样就符合 $(z)\vee(y)$ 的形式了。

第二步，将 $z$ 替换为 $\neg(A)$ ， $y$ 替换为 $A$ ，则 P4 变换为：

((x)\rightarrow(A)) \rightarrow (((\neg(A))\vee(x)) \rightarrow ((\neg(A))\vee(A)))

接下来，我们想要取合适的 $x$ ，使得 $(x)\rightarrow(A)$ 和 $(\neg(A))\vee(x)$ 都可被证明。

这里需要注意，公理和 MP 中都没有出现 $\neg$ 符号，所以需要再把 $(\neg(A))\vee(\neg(x))$ 转换为 $(A)\rightarrow(x)$ ，才能证明这一条。

转换到这一步，再对比一下公理 P1 和 P2 就比较显然了：

P1： $((x)\vee(x)) \rightarrow x$
P2： $(x) \rightarrow ((x)\vee(y))$
需要证明 1： $(x)\rightarrow(A)$
需要证明 2： $(A)\rightarrow(x)$

这里直接取 $x$ 为 $(A)\vee(A)$ ，两个需要证明的式子正好就是公理 2 和 1。思路到这里就完成了。

下面按照形式系统整理一下思路：

L1，在公理 P1 中，取 $x$ 为 $A$ ，有： $((A)\vee(A)) \rightarrow A$
L2，在公理 P2 中，取 $x$ 为 $A$ 、 $y$ 为 $A$ ，有：

(A) \rightarrow ((A)\vee(A))

L3，在公理 P4 中，取 $x$ 为 $(A)\vee(A)$ 、 $y$ 为 $A$ ， $z$ 为 $\neg(A)$ ，有：

(((A)\vee(A))\rightarrow(A)) \rightarrow \\ (((\neg(A))\vee((A)\vee(A))) \rightarrow ((\neg(A))\vee(A)))

L4，使用 MP，根据 L1 和 L3 可推出：

(\underline{(\neg(A))\vee((A)\vee(A))}) \rightarrow (\underline{(\neg(A))\vee(A)})

使用 IMPLY，将 L4 的 $\rightarrow$ 的两边整理为：

(\underline{(A)\rightarrow((A)\vee(A))}) \rightarrow (\underline{(A)\rightarrow(A)})

L5 使用 MP，根据 L2 和整理后的 L4 可推出：

(A)\rightarrow(A)

证毕。

# 形式系统的相容性、完备性

如果形式系统对于任意逻辑命题 $A$ ，都不能证明 $A$ 和 $\neg A$ （非 $A$ ）在该形式系统中均存在形式证明（即， $A$ 与 $\neg A$ 最多只有一个存在形式证明），则称该形式系统相容。

如果形式系统对于任意逻辑命题 $A$ ，都能证明 $A$ 和 $\neg A$ 至少有一个存在形式证明，则称该形式系统完备。

# 哥德尔不完备定理

# 定理的内容

哥德尔不完备定理分为两条，维基百科对定理的描述比较抽象，所以我把《数学女孩 3》中对定理的描述也摘录了下来：

维基百科 (opens new window)的描述：

哥德尔第一不完备定理：任何逻辑自洽的形式系统，只要蕴涵皮亚诺算术公理，就可以在其中构造在体系中不能被证明的真命题，因此通过推理演绎不能得到所有真命题（即体系是不完备的）。

哥德尔第二部完备定理：任何逻辑自洽的形式系统，只要蕴涵皮亚诺算术公理，它就不能用于证明其本身的自洽性。

《数学女孩 3》的描述：

哥德尔第一不完备定理：满足以下条件的形式系统是不完备的。

哥德尔第二不完备定理：满足以下条件的形式系统不存在“自己的相容性”的形式证明。
条件为：相容性、蕴含皮亚诺算术公理、还要是递归的

# 第一定理的证明思路

我们可以通过对形式系统的每个符号进行编码，就可以用自然数表示形式系统中的每个逻辑公式、形式公理、形式证明。哥德尔基于皮亚诺公理给出了一套构造方法（因此定理中的形式系统需要蕴含皮亚诺公理），我们将这套方法下的逻辑公式等对应的自然数称为哥德尔数。

定义了形式系统如何编码后，我们可以构建一个谓词 $f(x)$ 判断自然数 $x$ 是否是某个逻辑公式的哥德尔数。这个 $f$ 就被称为逻辑公式测定仪。同理也可以构建公理测定仪、测定证明仪和可测定性证明仪。

以上两步是用“算术”定义“形式系统”。

此外，我们也像定义形式系统 $H$ 那样，用“形式系统”定义这里的“算术”。具体来说，就是在形式系统中，定义表示“逻辑公式测定仪”的逻辑公式、表示“证明测定仪”的逻辑公式等。

因此，这里形成了一个闭环，我们定义了形式系统，又构建了形式系统的算术，最后构建了形式系统的算术的形式系统，也可以称为形式系统的形式系统。

最后一步，我们将一变量逻辑公式的哥德尔数，代入该逻辑公式的变量，便完成了逻辑公式的对角化，通过对角化构造了自指。

哥德尔通过将语句对角化，从而证明了第一不完备定理。他先构造了一个含有自由变量 $y$ 的逻辑公式 $p$ ：

$p$ : 将哥德尔数为 $y$ 的语句对角化后的新语句不存在形式证明。

这里“ $y$ 的对角化的语句”是通俗的说法，严谨的说法是“ $\text{subst}(y,\boxed{y},\overline{y})$ ”，即将 $y$ 的哥德尔数 $\overline{y}$ ，代入 $y$ 中的自由变量 $\boxed{y}$ ，得到的新语句。

然后将 $p$ 的哥德尔数 $\overline{p}$ 代入 $p$ 中的自由变量 $y$ ，并命名新的语句为 $g$ ：

$g$ : 将哥德尔数为 $\overline{p}$ 的语句对角化后的新语句不存在形式证明。

将 $p$ 的哥德尔数 $\overline{p}$ 代入 $p$ 中的自由变量得到的语句，正是“ $p$ 的对角化的语句”。也就是说， $g$ 正是将哥德尔数为 $\overline{p}$ 的语句对角化后的新语句！进一步说， $g$ 的含义可以解释为：

$g$ : $g$ 不存在形式证明。

在系统相容的前提下，我们既不能说语句 $g$ 存在形式证明（如果存在形式证明，则 $g$ 描述的 “ $g$ 不存在形式证明”就成立了），也不能说它的否命题存在形式证明。因此该形式系统是不完备的，哥德尔第一不完备定理得证。

哥德尔的证明的妙处在于，通过将逻辑公式转换为哥德尔数，再用数生成关于形式系统的谓词，实现了自指（Self-Reference，罗素悖论 $x \not\in x$ 也是基于自指），证明了系统的不完备性。而其它存在同样的自指的形式系统都是不完备的。

哥德尔第一不完备定理的证明思路就是如上，至于如何定义形式系统、定义哥德尔数、使用形式系统构造语句 $g$ 、使用形式证明和反证法推出矛盾，整个过程相当复杂、细节相当多。

而哥德尔第二不完备定理的证明需要第一不完备证明过程的中间产物，其证明思路，就不展开讲了。（说实话，没看懂）

# 定理的用途

基于哥德尔第二不完备定理，可以判断形式系统间的强度关系。例如，假设存在形式系统 X 和 Y，如果形式系统 Y 能证明 X 的相容性，那么可以说形式系统 Y 更强。