该文使用编程语言重新实现了当年哥德尔用数学语言证明的不完备定律。
1+1=2是公理，那么公理可以证明吗？哥德尔说不可以，数学不能用自己来证明自己的公理。同样适合编程领域，有一些真理，您永远无法写下来作为算法。算法也不是万能的。
在过去的300年中，数学家和科学家都做出了惊人的发现，从而形成了一种伟大的模式。模式是统一的：以前被认为是截然不同的想法始终如一！
牛顿为物理学家揭开了序幕，他发现使我们扎根于地球的原因还在于使地球围绕太阳旋转的原因。人们以为热量是一种特殊的能量，但事实证明可以用力学来解释。人们认为电，磁和光是不同的，但是麦克斯韦发现它们可以用电磁场来解释。
达尔文对生物学家也是如此。事实证明，我们的下巴，鸟类的美丽羽毛，鹿茸，不同的花朵，雌雄同体，您如此喜欢糖的原因，鲸鱼游动不同的原因...所有这些都可以通过自然选择来解释。
数学家为统一进行了类似的战斗。他们想找到数学的“核心”原理，从中可以得出所有真实的理论。这将在一个简单的保护伞下将逻辑与算术等结合在一起。(banq注：数学=逻辑+算术，对数字敏感的人可能精于算术，不一定有强逻辑能力；数学成绩好可能是算术精算能力强，不代表逻辑能力强)
要了解这是什么意思，请考虑以下问题：我们如何知道3小于5？还是1比2早？这是我们信奉的“核心”原则（其正式名称称为“公理”），还是可以从更多核心原则中得出？数字是基本概念，还是可以从更基本的东西衍生而来？
数学危机
数学家在争取核心原理的斗争中取得了长足的进步。例如，一位名叫弗雷格（Frege）的绅士发现他可以制作一套可以代表几乎所有事物的集合理论。例如，对于数字，他可以执行以下操作：
在这里，他表示空集为0。1是包含0的集合的集合。2是包含1和0的集合的集合。由此他可以设置一个原则来获取“下一个”数字：只需将所有先前的数字包装在一个集合中即可。太酷了！弗雷格（Frege）能够接受并证明算术规则，例如“ 1 +1”，“数字是无限的”等。
这看起来很强大，但很酷，但是Bertrand Russell出现并一举打破了理论。
他使用弗雷格制定的规则做出了有效但荒谬的声明。他证明了类似于1 +1 = 3 的东西也是成立的；毕竟这只是一个陈述。但是，对于基础数学理论而言，这是灾难性的。如果您可以证明1 +1 = 3，那么您就不能真正相信由此基础产生的数学上的任何真实陈述。
这使数学家陷入了混乱。他们甚至把这段时期称为“数学基础危机”。
希尔伯特计划
为了解决这个问题，一位名叫希尔伯特（Hilbert）的数学家认为必须对数学这样的基本理论提出了一些要求。他说，该理论必须是一种新的语言，其规则必须满足两个主要限制：
- 该理论将需要能够证明任何真实的数学陈述。例如，假设语句1 +1 =2。如果该语言不能证明该语句，那么它当然不能证明所有数学。希尔伯特称这种完备性。语言需要完备性；
- 第二个硬性要求是它不能证明是错误的数学陈述。如果我们可以证明1 +1 = 3，那么一切都是徒劳的。希尔伯特称这种为一致性。语言需要保持逻辑一致。
罗素和怀特海
打破弗雷格理论的绅士伯特兰·罗素（Bertrand Russell）与阿尔弗雷德·诺斯·怀特海德（Alfred North Whitehead）共同开发了自己的理论。他们花了多年的时间来制作大量的作品，称为Principia Mathematica。
他们从编写具有一些简单规则的新语言（我们称其为PM）开始。他们遵循了这些规则，并证明了很多事情。让我们在这里看一下几乎无法阅读的证明（不用担心，您不需要了解本文的语法）：
该证明表明“ 1 + 1”确实等于“ 2”。花了两卷才得到这个结论。
他们的语言很密集，工作很费力，但是他们不断证明数学中的许多不同真相，就当时任何人都可以说的，没有矛盾。可以想象，至少从理论上讲，您可以奠定这个基础，并最终将其扩展到数学之外：您可以用纯逻辑对狗的行为或人类的思维进行编码吗？
哥德尔来了
看起来数学原理也可以作为数学自己的基础理论，但是直到哥德尔改变了这一观点。
他证明数学原理确实具有无法用该语言证明的真实数学陈述，数学原理是不完备的。
这真是令人吃惊，但他的证明甚至更进一步。他表明，希尔伯特计划背后的整个意图：寻找数学的形式基础是永远行不通。
很难相信一个人真的可以证明某事“不可能”发生-想象一下，如果有人告诉你我们永远不会比太阳系更远的旅行-你会怀疑地看着他们。
然而，哥德尔当时是……25岁，毫无疑问地证明了这项事业是不可能的。他这样做是为了证明，如果一种语言可以代表数字，那么必然会出现无法证明的陈述。
让我们再想一想：数字看起来很古朴且易于证明-仅“ 1”，“ 2”，“ 3” ...等等。人们认为我们最终可以写下人类的想法-想象他们看到我们无法证明有关数字的所有真相，一定感到震惊。
让我们看看哥德尔是如何做到的。
PM-Lisp
现在，罗素和怀特海的语言很难看懂。更改周围的某些符号没有任何危害。让我们将他们的语言映射到更适合程序员的语言：Lisp！
您可以想象Russell和Whitehead想到了一种类似Lisp的语言。它们的语法如下：
仅从这些符号，它们就可以代表所有自然数。如果他们证明该符号0像0一样工作并且该符号next像一个后继函数一样工作，则(next 0)可以表示1，(next (next 0))可以表示2，依此类推。
他们是这样写的1 + 1 = 2：
(= (+ (next 0) (next 0)) |
更多点击标题见原文
...
结论
哥德尔得出了一个惊人的结论：如果PM-Lisp是逻辑一致的，那么它就必须是不完备的。如果完备的，则必须是逻辑不一致的。(banq注：逻辑本身的一致性和逻辑语言的完备性是对立的)
因此，数学也具有不能被简化为公理的特质。在编程中，它转换为：有一些真理，您永远无法写下来作为算法。这就是哥德尔发现的本质。
他继续证明了一些更令人惊讶的事情。事实证明，他可以写一个类似的有效句子，说“我无法证明自己是一致的”。这意味着没有任何形式的系统可以单独证明它只能产生真实的陈述。
现在，这并不意味着一切都是徒劳的。例如，这可能意味着我们不能编写像狗一样思考的算法...但是也许我们不需要。神经元不知道狗对玩具的爱的方式，我们的算法也不必是：也许意识会以同样的方式出现为现象。“像狗一样思考”的想法不会被具体记录下来。
我们不能在一个系统中证明它是一致的，但是我们可以证明使用另一个系统。但这当然引出了一个问题：我们如何证明其他系统是一致的？等等！
我认为哥德尔的想法就像一个指南：它向我们展示了使用规范算法可以做的事情的局限性。我发现他的所作所为真有趣。罗素（Russell）和怀特海德（Whitehead）遇到了很多麻烦，以免在工作中出现自我参考。在某种程度上，哥德尔通过构建第一个“自我评估”语言来解决这个问题，并得出了一些令人惊讶的结论。
如果您想创建自己的哥德尔数字，这是Clojure中的快速脚本。
黑客新闻评论：
我是一位数学家，作者他花了很多时间思考Goedel定理和附近的话题。作者自嘲地说，他不是数学家，而是程序员。不用担心：这是我所见过的Goedel定理中最受欢迎的论述之一。一切都得到了非常准确的解释，没有在Goedel定理的上下文中经常提到的愚蠢的错误和虚假，甚至原始证明也以非常平易近人的方式进行了草绘，在获得所有关键思想与跳过之间取得了很好的平衡大部分分散注意力的技术方面（重要且有趣，但我认为只对数学家有用，哈哈）。工作很棒。
这实际上是关于语言的概念。它证明没有语言可以是完备的。因此，即使存在，我们也无法表达出完备的系统。因此，很可能存在所有事物的统一理论，但是您将无法描述它。这是一个很好的哲学谜语。
对于普通读者来说，这是对哥德尔不完备性定理的一个很好的解释。
我已经读过Godel，Escher，Bach。这是一个很好的解释。