写给程序员的哥德尔第一不完备性定理

哥德尔的不完备性定理被誉为「20 世纪最伟大的数学发现」——事实上，这些定理不仅适用于数学，还适用于一切形式系统，并对科学、逻辑、计算机科学、哲学等领域有着深刻的影响。在这篇文章里，我会给出哥德尔第一不完备性定理一个简单但严谨的论证梗概。它的形式化表述是：

任何一致的形式系统 $S$，只要其中能够进行「一定量的初等算术」，就是不完备的；也就是说，$S$ 的语言中存在一些命题，既无法在 $S$ 中被证明，也无法被证否。

这是一个严谨的证明，重点面向软件工程师和程序员。这篇文章基于我不久前在 YouTube 上找到的一场精彩讲座。我第一次学习如何证明哥德尔不完备性定理，是在一门元逻辑课上，当时涉及各种令人困惑而深奥的话题，比如 Henkin 构造和超穷逻辑（transfinitary logic）。但事实证明，理解哥德尔并不需要这么大费周章！

引言

我们的旅程从定义几样东西开始。首先，我们把 $F$ 定义为一个函数，接受一个正整数，返回 0 或 1。下面是这样一个 $F$ 的例子：

于是，我们看到 $isOdd(2)=0$，或者 $isOdd(38943981)=1$。我们可以随意定义 $F$——只要它的输出要么是 0，要么是 1。设 $Q$ 为所有这类函数 $F$ 的集合。

如果存在一个计算机程序（或证明）$P$，接受输入 $x$ 并返回 $F(x)$，我们就说 $F$ 是可计算的。不言而喻，$P$ 必须在有限时间内完成，而且必须正确。那么来看点代码吧。$isOdd(x)$ 是可计算的吗？

function isOdd(x) {
  return (x % 2);
}

看起来是的！$x$ 为偶数时这个程序总会返回 0，为奇数时返回 1。再看一个更复杂的例子：

$isPrime$ 是可计算的吗？

function isPrime(x) {
  if(x < 2) return 0;
  if(x == 2) return 1;
  for(var i = 2; i < x; i++) {
    if(x % i === 0) return 0;
  }
  return 1;
}

多亏了这个 Stack Overflow 回答，看来它确实是可计算的。设 $A$ 为 $Q$ 中所有可计算函数的集合。我们（费了些力气）刚刚发现 $isOdd$ 和 $isPrime$ 都在 $A$ 里——也就是说，它们是可计算的。

但真正的大问题来了：$Q$ 中所有函数都是可计算的吗？或者等价地说：

如果 $A=Q$，那哥德尔就错了，所以我们需要想出一个巧妙的办法来证明 $A\subset Q$。换句话说，我们需要证明，存在一些函数，以正整数 $x$ 为输入、返回 0 或 1，却是我们根本无法实现的。

铺垫

那么，怎么证明某些函数 $F$ 是不可计算的呢？好吧，我们用最朴素的办法来做。既然我们已经在用 JavaScript，那就干脆把每一个 JavaScript 程序统统打印出来。是的，所有的程序。为了方便，我们可以按字母顺序和长度（即字典序）排列它们。为了更省事，我们可以直接扔掉那些会无限循环、或者不返回 1 或 0 的程序。等一切尘埃落定，我们剩下的是无穷多个程序，它们大概是这样开头的：

function F1(x) {
  return 0;
}

function F2(x) {
  return 1;
}

再往后……

function Fn(x) {
  return 1 - 1;
}

再往后……

function Fn(x) {
  return x / x;
}

再往后……

function Fn(x) {
  return (x % 2); // hey, this is the isOdd function from before!
}

再更往后……

function Fn(x) {
  return (x % 2) / 1;
}

再更往后……

function Fn(x) {
  let someRandomVariable = x ^ x;
  let abcd = someRandomVariable / y;
  if (abdc > -12) return 0;
  return 1;
}

你大概明白了。现在我们有了每一个用 JavaScript 写出、输出 0 或 1 的可能程序。换句话说，我们刚刚填满了 $A$：现在每一个可计算函数都对应着一个程序。让我们把它们放进一张叫 $T$ 的大表里。列标题表示输入（正整数），行表示可计算函数（以及隐含的、实现它们的程序）。

你会注意到 $isOdd$ 和 $isPrime$ 也进了我们的表（分别作为 fo 和 fp）。到目前为止一切顺利。看起来我们想到了所有情况。但让我们定义一个新函数：

其中 $f_i$ 是表 $T$ 中的第 $i$ 个函数。首先，让我们确认一下 $\bar{f}$ 是良构的。输入 $i$ 是一个整数。既然 $f_i$ 在 $T$ 中有对应的一行，$f_{i}(i)$ 就会返回 0 或 1。最后，$1-0=1$ 或 $1-1=0$，所以两种情况都是良构的。

因此，$\bar{f}$ 在 $Q$ 里，但它在 $T$ 里吗？

证明

要看出 $\bar{f}$ 为何不可能在 $T$ 里，其实相当直接。假设 $\bar{f}$ 就是 $f_2$。正如我们目前所见，$f_2(2)$ 要么是 0，要么是 1。但如果 $f_2(2)=0$，那么 $\bar{f}(2)=1−f_2(2)=1−0=1$。于是我们有：

糟糕。好吧，那它不是 $f_2$。那样也太容易了。那 $f_{421}$ 呢？如果 $f_{421}(421)=1$，那么 $\bar{f}(421)=1−f_{421}(421)=1−1=0$。于是我们有：

事实证明，无论我们从 $T$（以及隐含的 $A$）中挑出哪个可计算函数，它都会在至少一个输出上与 $\bar{f}$ 不一致。因此，我们得到了一个惊人的结论：

结语

换句话说，存在某些东西，比如 $\bar{f}$，是我们在形式系统中既无法证明也无法证否的。鉴于本文一直在用 JavaScript，一个程序无法在 $T$ 中引用它自己的字典序索引，这也就说得通了。话虽如此，你可能会忍不住想，或许有办法「绕开」这个限制；只要你的语言足够聪明，也许就行。我以后会写一写哥德尔第二不完备性定理，它会给这口棺材钉上最后一颗钉子：根本无法绕开。