素数的形式化表述

素数

稍微学过数学的人都很清楚素数（质数）这一概念，它被定义为：在大于1的自然数中，除了1和它本身以外不再有其他因数。

比如说，2、3、5、7、11……

形式系统

形式系统就不那么接地气了，恐怕没几个人听说过。我们可以把形式系统当做数学中的公理系统。回忆数学课本上的定理是怎么出现的：

给定公理1、公理2；
计算、推导；
得到结论，即定理。

这里的公理是不需证明的定理，中间的推导过程是对公理的合乎规则的操作，定理则是推导出的新的结论，整个过程即是“证明”。

形式系统与公理系统类似，其实，形式系统是对公理系统的形式化抽象。形式系统由三大要素构成：形式语言、推理规则和公理集合。

我们很容易将这三个要素与前面定理的证明过程联系起来。形式语言是公理和定理的载体，或者说是它们的表示形式；推理规则是推导过程中必须遵守的规则；公理集合是给定的所有公理的集合。

这些话都太过于抽象，不能再多说下去了，我们还是看看如何构建一个可以表示素数的形式系统吧。

素数的形式化表述

我们要构建一个形式系统，该形式系统的定理都写作Px。其中x是由任意多个'-'组成的字符串。

这里的Px就是所谓的形式语言，符合Px形式的字符串在该形式系统中被认为是有意义的。但有意义的字符串并不一定都是定理，我们规定，只有当x中的'-'数目为素数时，Px是一个定理，否则Px无意义。比如，P---是个定理，而P----则不是。

现在，我们得想出一些规则来产生有效的Px了。

回到现实世界，要想判断一个数N是否是素数，只需要判定N是否能够整除2～N-1之间的任何一个自然数，如果都不能，那么N是素数，否则不是。用形式话的语言表述这件事并不容易，我们需要能够判定整除的规则，然后是判定一个数不能被2~N-1之间任意一个数整除的规则，最后得到这个数是素数。

第一步，不可整除性：

定义1：xBZCy，其中x和y是'-'组成的字符串。
规则1：若xBZCy是个定理，则xBZCxy是个定理。

我们可以把定义1的含义理解成y不能被x整除。那么规则1就可以理解为，如果y不能被x整除，那么x+y也不能被x整除。

第二步，连续不可整除性：

定义2：zMYx，其中z和x是'-'组成的字符串。
规则2：如果--BZCz是个定理，则zMY--是个定理。
规则3：如果zMYx与x-BZCz都是定理，则zMYx-是个定理。

我们可以把定义2的含义理解成在2和x之间没有能整除z的数。那么规则2可以理解为，如果z不能被2整除，那么在2和2之间没有能整除z的数。规则3可以理解为如果在2和x之间没有能整除z的数，且z不能被x+1整除，那么在2和x+1之间没有能整除z的数。有点数学归纳法的感觉了吧。

第三步，素数：

规则4：若z-MYz是个定理，则Pz-是个定理。
公理：P--。

规则4可以理解为，如果在2和z之间没有能整除z+1的数，那么z+1是素数。这正是我们想要的素数的定义！当然，不要忘了最后一条公理，2是素数。

大功告成了，之所以把一句话拆分成这么多条复杂的定义和规则，就是为了能够形式化、没有歧义地构造素数的判定过程。

我知道看到这里的人肯定是懵逼的，上面写了些什么，其实我也没能全部理解。但无疑形式系统是很有趣的，它可以让我们用数学的方法描述世界。如果你注意到我在解释规则的时候都用了“可以”这个词，就能想象其实形式系统并不是那么具体，它既可以这样解释，也可以有其它不同的解释。所以说形式系统是一种抽象，是对任何事物的逻辑抽象，这也是数学的强大之处。

参考资料

《哥德尔、艾舍尔、巴赫：集异壁之大成》 侯世达
【数理逻辑如何入门】：公理系统和形式系统 豆瓣/逻辑