学习过程中非常害怕一种固定思维，特别是我们初心者对于很多东西容易陷入别人告诉你什么就是什么的节奏，这其实是非常不利的。这两年来的学习真是让我一次又一次的认识到这一点。
今天让我们来重新审视一下一个计算机中最最基本的一个概念：
自然数
我们初学计算机的时候总是被灌输一个概念那就是计算机之所以能够描述数字的计算这一过程是因为可以使用二进制，而数字电路课更是展示了二进制下基本计算结构ALU的简单构成。但是我们似乎还从来没有问过自己: 到底计算是什么？ 数字又究竟是什么？
接下来我希望能展示一种看待数字的不一样的观点。首先，需要指出的是计算机本质上是一种形式系统，而我们熟知的图灵机正是这样一种形式系统的模型，我们编程这一行为本质上是对于计算这种行为进行形式化抽象的一种过程， 而世界上的形式系统是多种多样的，所以抛开之前所有对于计算机的认知吧！在接下来的讨论中，数不再是天然存在的了，而是我们人为定义的啦。
说了这么多废话到底什么是自然数呢？ 0，1，2，3......这些数字在逻辑上到底有什么联系呢？
通过简单的观察我们不难发现自然数存在一个最小值0，并且所有的数n都有一个比自己大1的后继数 n+1。从数据结构的角度来说我们可以使用递归的方式来定义这个代数数据结构（Algebra data structure）
Inductive nat : Type :=
| O
| S (n : nat).
O (* 0 *)
(S O) (* 1 *)
(S (S O)) (* 2 *)
也许你不熟悉Gallina语言的语法但是相信上面的代码不难看懂
这种表示的方法把自然数的类型定义的更加精确了。
从证明理论（Proof ）和 系统验证（System Verification）的角度来说，一般语言中的自然数没有办法拿来研究自然数本身所具有的一些命题如加法的结合律（associate）。原因很简单，我们证明的过程是找到某个命题（一种类型）的一个证据（值），这时候我们需要每一个数是一个类型。比如
Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
intros n. simpl. reflexivity.
Qed.
暂时不想多写关于Coq语法上的东西，有空补上吧，这里也不需要关心Proof的内容
这当然不是我想出来的，第一个想到这种表示方法的人是 19世纪的伟大数学家(英灵) Giuseppe Peano 中文名叫做皮亚诺，是的你肯定在高数课上见过他的名字2333333皮亚诺余项。其实计算机和数学的联系是非常非常深的，但是似乎现在国内的计算机教学从来没有让学生去接触这些特别基础的部分。
作为一种形式系统的组成部分，皮亚诺的野心当然不止是定义自然数那么简单，为他们添加规则是肯定的。
- ¬(0 = x + 1)
- x + 1 = y + 1 → x = y
- x + 0 = x
- x + (y + 1) = (x + y) + 1
-
P(x) 是一个带自由变量x的一阶逻辑表达式(first-order formula ) 有如下公理
(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y).
是的我们现在有加法啦！！满足上面几条公理(Axiom)的形式系统被称为带 Presburger Arithmetic的系统。
这里请允许我简单的再加一些关于形式系统的小知识，一个形式系统主要有3个特性
- 完备性(complete): 这是说任何一个系统中结论或者说定理可以由已经有的定理通过有限的步骤推理得出。
- 一致性(consistent) 系统中得出的新结论不会和已经有的矛盾。
- 确定性(decidable) 存在一种算法可以判断一个定理到底是不是真的。
而我们的Presburger Arithmetic
是decidable的！！！
这意味着在这个形式系统当中任何一个自然数相关的定理，可以判定到底对不对，在也没有什么上帝魔法啦。至于如何证明，需要牵扯eliminator相关的理论，在这里先不讨论吧。
emmmmmmmmmm好像标题是Peano Arithmetic，之前说的伟大数学家也是Peano，这个怎么不是他的名字。。。
那是因为皮亚诺的设想更加的有野心，他给出的是一个更加强的约束。
- 0是一个数
- 如果a是一个数，那么他一定有一个后继(successor)，同样是个数
- 如果两个数的后继一样，那么他们一样
- 如果一个数的集合S中存在0，并且每个数的后继数在S中，那么每一个数都在S中(这条叫归纳公理Induction axiom, 其实就是可以用数学归纳法的意思)。
看起来很简单，没有具体的去定义运算，只是说我们可以归纳，但是这其实已经涵盖了自然数相关的几乎所有命题。如果Peano Arithmetic是一致，确定，完备的，那么数学家可以下岗了，所有这相关的数学命题都以用计算机来证明或证否了。
数学家和计算机科学家们当然木有下岗,这被证明是不可确定的。。。。。
而后一个伟大人物的出现了----------哥德尔(Kurt Friedrich Gödel),求求FGO快点实装。
他给出了更加强大的结论
- 任意一个包含一阶谓词逻辑与初等数论的形式系统，都存在一个命题，它在这个系统中既不能被证明为真，也不能被证明为否。
- 如果系统S含有初等数论，当S无矛盾时，它的无矛盾性不可能在S内证明。
这直接说明了带皮亚诺算术或是ZFC就有不可判定的命题了。。。。。
完了全特么完了。。。。。。。
只能说如果上帝真的存在, 他估计带了皮亚诺算术吧
网友评论