数学倒底有没有绝对的严格性和形式化？

我对数学的理解只停留在大学里的高等代数和微积分，而且毕业后的这 8 年也已经遗忘得差不多了。最近在研究算法，又不得不拾遗和学习一些数学知识。今天这篇文章，希望和大家讨论一个问题：数学到底是否具有绝对的严格性和形式化？恕我愚钝，这个问题让我有点懵了。

之前我只是想了解一下图灵机，结果在查资料的时候偶然知道了数学的三次危机，发些这些数学历史还满有趣的，对理解图灵机也有帮助，然后就把它写到文章 《算法02 - 从罗素悖论到图灵机》 中去了。

在文章中讲“哥德尔不完备性定理”时，有一段这样的描述：

哥德尔不完备性定理的证明结束了关于数学基础的争论，宣告了数学不是绝对严格性的，把数学彻底形式化这种愿望是不可能实现的，不存在这样一个完美的数学系统。

说实话，在写这篇文章此之前，我一直认为数学是具有绝对的严格性的。但在我查关于数学的三次危机历史的时候，知道了哥德尔不完备性定理，才认为数学不是绝对的严格性和形式化的。

文章发布后有位博客园园友[窗户]在文章留言，引发了我的重新思考，原文如下：

哥德巴赫猜想的简称应该是 1+1，不是 1+1=2，那是以讹传讹的说法。再者，至今没有人证明哥猜是不可判定命题。谁说数学不是彻底严格的?谁说数学不是彻底形式化的?绝对的严格，形式化，本来就是数学的特征，和系统完备性没什么关系。如果非得说完备的形式系统才是完美的，那其实这样的形式系统也是有的啊，比如一阶逻辑就是，只是小了那么一点而已。

必须得说，园友[窗户]在数学方面的理解和学习应该是比较深入的，至少是比我厉害很多的。在看到[窗户]的评论时，我都不知道“一阶逻辑”是什么。另外，我还看了下园友[窗户]的博客园，分享的都是很有深度的文章，他是一个数理逻辑非常强的人。

这使我我不禁又开始怀疑起自己的理解：目前为止，数学到底是否具有绝对的严格性和形式化？

带着疑惑，我又向园友[窗户]提了一问：

数学要在我们已知的定理和概念的基础上才能是绝对的严格和形式化吧？否则，你怎么解答“集合 S 由一切不属于自身的元素组成，那么 S 是否属于 S 呢？”这个问题呢？

然后园友[窗户]回复了我：

悖论的原因，在于形式化过程中公理设定的问题，建立的公理存在矛盾才会导致悖论，这样的“系统"是不相容的,从而我们并不认可。另外，不可判定，哪是什么到现在为止没人解决。简直很扯啊。不可判定是命题自身的属性，跟人能不能解决没关系。呵呵，假如有天有人把哥猜解决了又怎么办？

我就更疑惑了，既然“不可判定是命题自身的属性”，那反而不就更说明了数学的不严格吗。思考了一段时间后，我觉得可能问题出在我和园友[窗户]理解的出发点不同上面，但不知道谁是对的。然后我就回复了我的理解：

我觉得我和你的理解，前置条件是不一样的。你的理解是数学是在已知的定理和概念的基础上建立的，这样自然是具有严格性的，因为每一个命题都是人类从已知的定理或概念严格推导出来的。但也正如你所说，“不可判定”是命题自身的属性，用人类已知的定理并不能证明所有的命题是真或是伪。如果能的话，那数学才真的是具有了绝对的严格性（这是我的理解）。所以后来人们才会引入“计算模型”，用来区分哪些命题是可证的，哪些命题是不可证的。假如有天有人把哥猜解决了又怎么办？那说明数学离绝对的严格性又近了一步呗。

完了我又继续补充了一句：

在人们的信念中，数学是应该具有绝对的严格性和形式化的，还在一直在探索中。但目前数学从上到下还没有实现成为一个完整的体系，还没有绝对的严格性和形式化。

几经来回思考，站在我理解的出发点，我虽然说服了自己，但心中还是没有底，可能我理解的出发点就错了。不是有这么一句话么，人最可怕的就是不知道自己不知道。

真切地希望有人能帮助解答这个问题，不甚感激。

非常感谢博客园园友[窗户]的热心讨论。

-------------------------------------------------------------

昨天在我写完本文的以上内容后，并已在公众号发布，截止昨夜，园友[窗户]再次回复了我，内容是这样的：

看了你的论述，我忍不住还是回来论述几句。你似乎要把数学代入一种哲学的范畴，一切变得模棱两可。已知的定理和概念指的是什么?不知道你明白不明白定理和公理的区别，我猜测你的意思可能是指公理和已经从公理演绎出的定理。描述模棱两可的原因，我想是因为你并未严格意义上受过数学学习，那么你对于数学的理解我也是可以理解的。计算模型呢，你要真说是因为这个，我也不能算你错，因为计算和演绎本质上算是一回事。递归论之所以是数理逻辑中的学科，也正是因为计算和演绎本质相同。完备性和严格性(换成相容性我觉得可能更合适)并不是一回事，严格的意思在于无歧义。从这一点来说，你的理解是有偏差的。

 “严格的意思在于无歧义”，我觉得这一点说得很对，因此我也能理解数学是绝对严格性的说法。但我依然还是认为数学目前是没有绝对形式化的，否则罗素悖论在集合论的范畴确实是解释不通的。你们认为呢？