皮亚诺自然数理论中的两类归纳法

今天被问及 Peano 自然数理论中良序性和第二类归纳法（强归纳法）的关系，没有记清楚良序性的严格定义，也没能答出与第二类归纳法的关系，感觉还是没读进去...所以本文是再回顾 Peano 自然数理论做的整理。

皮亚诺公理

由于第一类归纳法与公理第五条直接相关，首先我们需要回归一下完整的皮亚诺公理

• PA1. \(0 \in \mathbf{N}\).
• PA2. 若\(x \in \mathbf{N}\)，则\(x\)有且仅有一个后继\(x'\).
• PA3. 对任一\(x \in \mathbf{N}\)，皆有\(x' \neq 0\).
• PA4. 对任一\(x,y \in \mathbf{N}\)，若\(x \neq y\)，则\(x' \neq y'\).
• PA5. （归纳公理）设\(M \subset N\). 若\(0 \in M\)，且每当\(x \in M\)也有\(x' \in M\)，则\(M = N\)

两类归纳法

现在给出两类归纳法的描述

（第一类归纳法）设关于自然数的任一命题\(p(n)\) 满足下列条件 1,2，则对于所有的\(n\)，\(p(n)\)成立

1. \(p(0)\)成立
2. 每当\(p(x)\)成立，都有\(p(x')\)成立

第一类归纳法就是我们常说的数学归纳法（高中即见过），而第二类归纳法也有习惯称之为强归纳法。

（第二类归纳法）设关于自然数的任意命题\(p(n)\)，满足下列条件 1,2，则对于所有的\(n\)，\(p(n)\)成立

1. \(p(0)\)成立
2. 当\(k<x\)都有\(p(k)\)成立，则\(p(x)\)成立

归纳法的证明

第一类归纳法的证明

其实根据归纳公理，我们很容易得出第一类归纳法的正确性，所以第一类归纳法实际上就是跟皮亚诺公理直接相关的。归纳公理 PA5 所断言的，恰是\(\mathbf{N}\)这个抽象的自然数集的最小性。

（第一类归纳法）...

证明

设\(M = \{x \in N ~|~ p(x) \}\).

1. 根据归纳假设 1，\(p(0)\)成立，则\(0 \in M\).
2. 而根据归纳假设 2，\(x \in M \rightarrow x' \in M\).

根据归纳公理（PA5），我们得到\(M = N\)，即说明该关于自然数的全称命题得证。

第二类归纳法的证明

第二类归纳法的证明显然没有作为一条额外的公理加入到皮亚诺公理集中，这说明我们需要另找一条路子利用已有公理定理给出强归纳法的证明。

一般的教材都会由现有公理正向推理（forward reasoning）得出正确证明，不过这里我们最终的落脚点在第二归纳法的证明，类似定理证明器（比如 Coq）的机器证明常采用的逆向推理（backward reasoning）的方式。我后面的叙述通过“倒叙”的方式，由最终的证明一步步联系起必要的 Lemma，引出和良序的关系。

（第二类归纳法）...

证明

设\(M = \{x \in \mathbf{N} ~|~ \lnot p(x) \}\)，则命题等价于\(M\)为空，

反设\(M\)不为空。根据\(\mathbf{N}\)的良序性（我们需要的定理，即若\(L \subset \mathbf{N}\)，\(L \neq \emptyset\)，则\(L\)必有最小数）。\(M\) 集有最小数 \(m\)。这里分情况讨论显然\(m\)不为\(0\)（\(0\)的情况直接与归纳假设 1 矛盾），另一情况的讨论如下

1. 根据归纳假设 1，\(p(0)\)成立
2. 由于\(m\)是\(M\)的最小数，则任一\(k<m\)，均有\(p(k)\)成立，根据归纳假设 2，\(p(m)\)成立，与\(\lnot p(m)\)矛盾。

故假设不成立，\(M\)为空，原命题得证。

这里我们看到，应用了良序性，而引入良序概念与证明，又要求我们引入可比性相关的定理。

（良序性）若\(L \subset \mathbf{N}\)，\(L \neq \emptyset\)，则\(L\)必有最小数。

最小数的概念是从可比来的，需要我们建立自然数上序的概念。这里略过，有兴趣的同学可以再去查阅自然数上的序（小于等于）是如何定义的。

\(L\)中有最小数，我的理解是（形式化表达）\(\exists y( y \in L \land \forall x(x \in L \rightarrow y \le x))\)

（良序性）

证明

设\(M = \{ x \in \mathbf{N} ~|~ x 是 L的下界 \}\)，即\(M\)中的元素都是\(L\)集的下界，原命题等价于\(L \cap M \neq \emptyset\)

反设\(L \cap M = \emptyset\)，对\(x\)进行归纳

1. \(0 \in M\) （\(0\) 显然是下界）
2. 当\(y \in M\)，因\(L \cap M = \emptyset\)，则\(y \notin L\)，所以对任一\(x \in L\)，都有\(y < x\)，而这可以得到\(y' \le x\)（这里又是使用了一条待证的定理），所以\(y' \in M\)

根据归纳公理，我们可以得到\(M = \mathbf{N}\)，而又由于\(L \subset L\)且\(L \neq \emptyset\)，那么自然数集一个不为空的子集与自然数集相交，不应为空集，即\(L(实为 \mathrm{N}) \cap L \neq \emptyset\)，与假设矛盾。

故良序性得证。

待解决问题

1. 理解条件的“强弱”，与命题的“强弱”
2. 理解为什么用第一类归纳法直接说明第二类归纳法的证明是错误的。
3. 为什么 Coq 里使用第二归纳法需要添加有关反证和序的两个公理（注意 Coq 里是没有排中律的）。