哥德尔证明

一个成功的一致性绝对证明例子

形式系统

考虑一个简单的形式演算系统。

符号集

符号集包含命题变量 \(p,q,r\) 等,符号常量为 \(\sim, \lor, \to, \land\),以及标点符号 \((, )\)。这些符号都是我们平时使用的含义。

公理

这个演算系统的公理为下面四个。

\[ \begin{align} (p \lor p) \to p \\ p \to (p \lor q) \\ (p \lor q) \to (q \lor p) \\ (p \to q) \to ( (r \lor p) \to (r \lor q)) \\ \end{align} \]

变换规则

  1. 替换规则:可以使用一个命题变量替换同一个公式里的某一个命题变量。
  2. 分离规则:如果 \(S_1\)\(S_1 \to S_2\),那么有 \(S_2\)

考察

公式 \(p \to (\sim p \to q)\) 是该形式系统的一条定理。假设,某一命题 \(S\) 以及其否定形式 \(\sim S\) 都能从公理中推导出来,那么通过使用替换规则和分离规则,可以得到公式 \(q\)

\[ \begin{align} p \to (\sim p \to q) \\ S \to (\sim S \to q) \\ \sim S \to q \\ q \end{align} \]

这意味着,如果有某个公式 \(S\) 及其否定形式 \(\sim S\) 都能从公理中导出,则任何公式都能从这组公理中导出。总之一句话,如果这个系统不是一致的,则每一个公式都是定理。反过来说,如果不是每个公式都是定理(即如果至少有一个公式不能从公理中推导出来),那么这个形式系统是一致的。

哥德尔编码

哥德尔描述了一种形式验算系统,我们称其为 PM,在其中能够表达所有的通常的算术概念,并建立熟悉的算术关系。

给每一个原始符号,每一个公式(或符号串)以及每一个证明(公式的有限序列)都指定一个独一无二的数是可能的。这个数可以看作是一种区别用的标签,被称为符号,公式或证明的“哥德尔数”。

编码方式如下

\[ \def\arraystretch{1.2} \begin{array}{c|c|c} 固定符号 & 哥德尔数 & 意义 \\ \hline \sim & 1 & 非 \\ \lor & 2 & 或 \\ \to & 3 & 如果 \cdots 那么 \cdots \\ \exists & 4 & 存在一个 \cdots \\ = & 5 & 等于 \\ 0 & 6 & 零 \\ s & 7 & \cdots 的直接后继 \\ ( & 8 & 标点 \\ ) & 9 & 标点 \\ , & 10 & 标点 \\ + & 11 & 加 \\ \times & 12 & 乘 \\ \end{array} \]

\[ \def\arraystretch{1.2} \begin{array}{c|c|c} 数字变量 & 哥德尔数 & 可能的代入 \\ \hline x & 13 & 0 \\ y & 17 & s0 \\ z & 19 & y \\ \end{array} \\ \]

数字变量与大于 12 的素数相联系

\[ \def\arraystretch{1.2} \begin{array}{c|c|c} 命题变量 & 哥德尔数 & 可能的代入 \\ \hline p & 13^2 & 0=0 \\ q & 17^2 & (\exists x)(x=sy) \\ r & 19^2 & p \to q \\ \end{array} \\ \]

命题变量与大于 12 的素数平方相联系

\[ \def\arraystretch{1.2} \begin{array}{c|c|c} 谓词变量 & 哥德尔数 & 可能的代入 \\ \hline P & 13^3 & x=sy \\ Q & 17^3 & \sim(x=ss0 \times y) \\ R & 19^3 & (\exists z)(x = y + sz) \\ \end{array} \\ \]

谓词变量与大于 12 的素数立方相联系

对应引理

每一个原始递归的真理,当用形式演算的符号将其编码为符号串时,都成为一条定理。其次,在一个接一个的基础上,形式符号配得上其约定的解释。

元数学的算术化

哥德尔证明有关形式演算中表达式的结构性质的元数学命题,能够被精确地映射到这个验算自身。他的这个做法的基本思想是:因为 PM 中的每一个表达式都对应一个特定的哥德尔数,因而关于表达式及其相互间排列关系的元数学命题,就可以被理解为关于与之对应的哥德尔数及这些数相互的算术关系的命题。用这种方法,元数学就变得完全“算术化”了。

一个简单的例子

一个简单的公式“\(\sim(0 = 0)\)”,它表达了一个明显的错误,即零不等于自己。

现在看一个简单的元数学命题:这个公式的第一个字符是“\(\sim\)

首先计算该公式的哥德尔数,称其为 \(a\),则有

\[ a = 2^1 \times 3^8 \times 5^6 \times 7^5 \times 11^6 \times 13^9 \]

由于 \(\sim\) 的哥德尔数是 \(1\),则该公式必然会有一个因子是 \(2^1\),所以这个元数学命题对应的一个数论命题是:\(**2\)\(a\) 的一个因数,但 \(2^2\) 不是**。

以上展示了如何用数论的方式来说我们的公式的第一个符号是波折号。下一步是,将这个用汉语说的命题,转换为 PM 的正式符号串。在 PM 中表达“\(x\)\(y\) 的一个因子”,可以表述为“\((\exists z)(y = x \times z)\)”。所以上面是数论命题可以表达为

\[ (\exists z)(\underbrace{ss \cdots ss}_{a\tiny 个}0 = z \times ss0) ∙ \sim(\exists z)(\underbrace{ss \cdots ss}_{a\tiny 个}0 = z \times (ss0 \times ss0) \]

综上,有一个 PM 的定理,它翻译了“\(\sim(0=0)\)’的开始符号是波这号”这个真的元数学命题。

一个复杂的命题

现在将注意力转向一个更为复杂的元数学命题:具有哥德尔数 \(x\) 的公式序列是哥德尔数为 \(z\) 的公式(在 PM 中)的证明。用 \(\text{dem}(x, z)\) 来表示 \(x\)\(z\) 之间的算术关系。从这个事实出发,通过哥德尔对应引理,在 PM 中有一个形式符号组成的公式表达了这个关系。用 \(\text{Dem}(x, z)\) 来指此公式。

哥德尔的对应引理表明,任何时候数论术语 \(\text{dem}(x, z)\) 为真时,形式为 \(\text{Dem}(\underbrace{ss\cdots ss}_{x\tiny 个}0, \underbrace{ss\cdots ss}_{z\tiny 个}0)\) 的字符串是(PM的)一个定理。

替换

考察公式 \((\exists x)(x = sy)\),其哥德尔数是 \(m\),而其中的一个变量 \(y\) 的哥德尔数为 \(17\)。用 \(m\) 替换 \(y\),将得到一个极长的公式

$ (x)(x = _{m + 1 个}0) $

这个新的 PM 字符串的意思是,存在一个数 \(x\)\(m\) 的直接后继。或者简单地说,\(m\) 有一个后继。这个公式本身又有一个哥德尔数,可以用一种元数学方式简单地刻画这个结果数:它是在一个哥德尔数为 \(m\) 的公式中,用 \(m\) 本身去替换其中哥德尔数为 \(17\) 的变量而得到的新公式的哥德尔数。用记号 \(\text{sub}(x, 17, x)\) 来代表新哥德尔数。它是老哥德尔数 \(x\) 的函数。

而由于 \(\text{sub}\) 函数是原始递归,所以在 PM 中存在一个恰好映射它的形式表达式,我们将这个表达式记为 \(\text{Sub}(x, 17, x)\)

论证的核心

  1. 在 PM 中构造一个公式 \(G\),使其表达以下元数学命题:“使用 PM 的规则,公式 \(G\) 不可证“。
  2. 证明,\(G\) 是可证明的,当且仅当它的否定形式 \(\sim G\) 是可证明的。如果一个公式及其否定都是形式可证明的,那么 PM 就是不一致的。反过来,如果 PM 是一致的,则 \(G\)\(\sim G\) 都不可能从 PM 的公理中推导出来。
  3. 尽管 \(G\) 是形式不可证明的,它却是真的算术公式。
  4. 由于 \(G\) 是真的,又是形式上不可判定的(在 PM 中),因此 PM 肯定是不完全的。换句话说,我们不能用 PM 的公理和规则导出所有的算术真理。并且,哥德尔进一步证明,PM 在本质上是不完全的。即使用附加的公理(或规则)来扩大 PM,使真公式 \(G\) 在增强了的演算中称为形式可推导的,也会有另一个用完全类似的方式构造出的真公式 \(G'\),而 \(G'\) 在增强的演算中是形式不可判定的。
  5. 哥德尔描述了怎样构造一个 PM 的公式 \(A\),它所表达的元数学问题是:”PM 是一致的“,并且证明公式”\(A \to G\)“在 PM 中是形式可证明的。最后,他表明公式 \(A\) 在 PM 中是不可证明的,从而得出推论,PM 的一致性是无法用任何系列的逻辑推理来证明的,只要这些推理是可以被映射在 PM 本身组成的形式演绎系统中。

第一步

公式 \(\text{Dem}(x, z)\) 在 PM 中表达了元数学命题:”哥德尔数为 \(x\) 的公式序列是哥德尔数为 \(z\) 的公式的一个证明“,在其前面加上存在量词,即 \((\exists x) \text{Dem}(x, z)\),这个公式表明:”哥德尔数为 \(z\) 的公式是可证的“。在其前方加上否定,即 \(\sim (\exists x) \text{Dem}(x, z)\),这个公式表示:”哥德尔数为 \(z\) 的公式是不可证的“。

需要做的是,证明这个公式的某个特例是不可证的。从下面的公式开始

\[ \tag{1} \sim (\exists x) \text{Dem}(x, \text{Sub}(y, 17, y)) \]

公式(1)表达了元数学命题:”哥德尔数为 \(\text{sub}(y, 17, y)\) 的公式不可证明“。但此时包含了变量 \(y\),接下来需要将变量换成一个数字。由于公式(1)属于 PM,所以这个公式有一个对应的哥德尔数,令其为 \(n\),用 \(n\) 来替代 \(y\),得到一个新的公式,称其为 \(G\),有

\[ \tag*{G} \sim (\exists x) \text{Dem}(x, \text{Sub}(n, 17, n)) \]

公式 \(G\) 表明的元数学问题是:”哥德尔数为 \(\text{sub}(n, 17, n)\) 的公式是不可证的“。公式 \(G\) 属于 PM,因此会有一个对应的哥德尔数 \(g\)。而 \(g = \text{sub(n, 17, n)}\)

令公式 \(\sim(\exists x )\text{Dem}(x, \text{Sub}(y, 17, y))\) 的哥德尔数为 \(n\),用 \(n\) 替代 \(y\) 得到 \(\sim(\exists x )\text{Dem}(x, \text{Sub}(n, 17, n))\)。而其中的 \(\text{Sub}(n, 17, n)\) 为”对于哥德尔数为 \(n\) 的公式,用 \(n\) 替换 \(y\) 得到的公式的哥德尔数“,这个数实际上是 \(\text{sub}(n, 17, n)\),而这样替换之后,得到的正是公式 \(G\),所以公式 \(G\) 的哥德尔数 \(g\) 就是 \(\text{sub}(n, 17, n)\)

但公式 \(G\) 表明的是”哥德尔数为 \(g\) 的公式是不可证的“,而 \(G\) 的哥德尔数是 \(g\)所以 \(G\) 实际上是说”\(G\) 是不可证的“

第二步

哥德尔证明了,如果 \(G\) 可证,则 \(\sim G\) 可证(因而 PM 不一致),而如果 \(\sim G\) 可证,则 PM 是 \(\omega\)-不一致的。一个更强的结果是后人 Rosser 在 1936 年得到的,也就是”\(G\) 是可证明的,当且仅当它的否定形式 \(\sim G\) 是可证明的“。

如果一个公式及其否定形式都能从 PM 中得出,那证明 PM 不是一致的。反过来,如果 PM 是一致的,则 \(G\)\(\sim G\) 均不可证,也就是 \(G\) 是不能判定的。

第三步

在 PM 一致的前提下,由于 \(G\) 说的是”\(G\) 是不可证的“,但实际上 \(G\) 是不能判定的,所以 \(G\) 说了真理,也就是 PM 的一个定理。

但不难看出 \(G\) 为真,因为在第二步才证明了 \(G\) 在 PM 是不可证的,而 \(G\) 表述的也是这件事情。

第四步

一个演绎系统被称作是”完全的“,如果每一个能在此系统内表示的真命题都是可以用演绎规则从公理中推导出来。如果不是这种情况,那么这个系统被称作”不完全的“。由于上面的步骤表明 \(G\) 是 PM 的真公式但又是在 PM 中形式不可推导,因此 PM 是一个不完全的系统(当然,假定的前提是 PM 是一致的)。

第五步

考虑一个元数学命题:”如果 PM 是一致的,则它是不完全的“。

上面的例子已经给出,如果一个形式系统是一致的,则会有至少一个公式是不可证的,所以上述命题的前半句,等价于说”至少有一个 PM 的公式在 PM 中是不可证的“。而对应的数论命题则是”至少存在一个 \(y\),没有一个 \(x\) 能和它构成 \(\text{dem}\) 关系“。

\[ \tag* A (\exists y) \sim (\exists x) \text{Dem(x, y)} \]

一个系统不完全,意味着存在真的但又不可证的公式 \(X\) 不是 PM 的定理。通过上面可知,\(G\) 正是这样的一个公式,它在 PM 不可证,但是确实真的。所以 \(A \to G\) 正是这个元数学命题的 PM 公式,也就是

\[ (\exists y) \sim (\exists x) \text{Dem(x, y)} \to \sim (\exists x) \text{Dem}(x, \text{Sub}(n, 17, n)) \]

可以证明这个公式在 PM 中是可以证明的。基于分离规则,如果 \(A\) 可证,那么必然会导致 \(G\) 也可证,但是 \(G\) 实际上不可证。因此,如果 PM 一致,则 \(A\) 在 PM 中是不可证的。

因此,假设通过一串推理步骤能非形式的证明 \(A\) 这个元数学命题,并且如果这一串步骤能映射为 PM 中构成证明的公式序列,那么公式 \(A\) 本身在 PM 中就是可证的。但正如我们刚看到的,如果 PM 是一致的,则这是不可能的。所以我们被迫得出结论:如果 PM 是一致的,那么它的一致性是无法用任何可被映射到 PM 自身的元数学推理来证明的。

这个哥德尔分析的辉煌结果不应被曲解:它并未排除 PM 一致性的元数学证明,它排除的是能被映射到 PM 内的一致性证明。