为设么丰卫兵说的“All software bugs can be fixed"是个伪命题。

丰卫兵的标题“All software bugs can be fixed"是个伪命题。

1。在“fix”之前，你先得知道哪里有bug，bug是什么。或者说，你定下你对一个程序的specifications，我写一个程序交给你，你要看这个程序能不能满足你的specifications，如果不能，那就有bug。既然你要做判断，就必须是数学上严格的判断。从Godel和Turing的理论可以推出：总存在很多程序，无法从数学上严格地判断它们到底会做些什么，包括存在不存在bug。

2。什么叫程序／软件，要用Turing machine来定义。简单地说，就是平时我们运行地那些，但是它们用的内存大小没有上限。注意，它们在任何时候用的内存量都是有限的，但是要多少有多少。其实这在今天的网络上用distributed computing已经近似地可能了，可以用到整个网络地所有内存。再往上去，理论的不可能和实践的不可能就没有区别了，不过我们还是看理论说些什么。

3。什么叫严格地判断？就是给出数学上地证明，说某个程序是对或错。数学的证明要用到一定的公理系统和逻辑推理法则。比如欧几里得几何就是建筑在五大公理之上，你也许曾读过关于第五条，平行公理的几千年的争论和研究。曾有许多人试图用其它四条公理证明这第五条，都失败了。其实这是不可能的，如果否认平行公里，也能得到一套自恰的非欧几何。目前数学界在数学基础方面用的公里体系是ZFC的集合论，Peano的自然数公理，和2nd－order逻辑推理体系。

4。Godel证明了：给定任何公理体系，不管多么地复杂，包含多么多条公理，只要这些公理是互洽的（不是互相矛盾），那么一定存在有关自然数的真命题（就是说，是对的命题），它们是证明不了的。这适用于目前的数学体系，也同样适用于任何对它的扩充。你即使把证明不了的命题加为新公理，仍旧有证明不了的东西，而且永远是无限多的。

5。很难证明的命题很多。费儿马大定理就是有关自然数的一个命题，十几年前才被Princeton的Wiles证明。哥德巴赫猜想，还有孪生素数猜想等等，都是还没被证明的有关自然数的命题。最难的恐怕是黎曼猜想了，要用到复变函数，现在有许多数学家在研究，估计75％是先证明他的，20％左右觉得它不对，想找反例，还有5％左右正是觉得它可能是一个证明不了的命题。

6。每一个有关自然数的命题都可以用一个程序去一个数一个数地验证。（作为练习，编个程序验证费儿马大定理，看有没有反例）。只要假设内存可以要多少有多少，那么理论上就是Turing machine，每个数都能验证到。对于这个命题，如果程序找到一个反例，那就以错误结束，成为一个bug，要么crash电脑，要么造成丰田车加速，随你怎样。如果还没有找到反例，那就正常地继续找，也继续正常地让你开丰田车，直至永远。

7。如果你能严谨地判断这样一个程序不会有错，那么你就证明了它对应的命题是对的。因此，应用Godel的结果就是：一定存在有关自然数的命题，它是证明不了的，用来核实它的程序也就是判断不了对错的。这样的程序是无限地存在的。

因此，“All software bugs can be fixed"是个伪命题。

下面说说为什么指出你的伪命题那么重要。原因是，从伪命题出发，公里系统就不是自洽的了，数学家证明了：不是自洽的系统可以把任何假命题“证明”成真的。这是另一个数学大家Russell证明的。据说有人不信，挑战他说：“Assume that 1=2, prove that I am the Pope.”结果Russell不假思索就回答了：“You and the Pope are two, therefore you and the Pope are one.”

丰卫兵想从伪命题出发，“推出”其它伪命题为丰田开脱。其心可诛。特正视听。