哥德尔不完备定理

由对角线引理(康托尔对角线论证的形式化近亲),算术可以构造一个句子 $G_F$ 满足 $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F\urcorner)$——一个断言自身在 $F$ 中不可证的句子。若 $F \vdash G_F$,则 $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ 成立,从而 $F \vdash \neg G_F$,与一致性矛盾。因此 $F \nvdash G_F$——而这恰恰就是 $G_F$ 所断言的内容,所以 $G_F$ 在 $\mathbb{N}$ 中为真。(罗瑟后来去掉了 $\omega$-一致性假设。)

第1步(语法的算术化)。固定一种可计算的编码方案,给 $F$ 语言中的每个符号、每个公式以及每个有限公式序列都分配一个唯一的自然数,即它的哥德尔数。由于 $F$ 是可有效公理化的,关系 $\mathrm{Prf}_F(p, n)$——"$p$ 是代码为 $n$ 的公式的一个证明的代码"——可以用一个只含 $+$、$\times$ 和量词的算术公式来表达,因为逐行检查一个证明是一个有限的机械过程。定义 $\mathrm{Prov}_F(n) := \exists p\, \mathrm{Prf}_F(p, n)$。

第2步(对角线引理)。对任意只含一个自由变量的算术公式 $\psi(x)$,对角线引理都能构造出一个句子 $D$,满足 $F \vdash D \leftrightarrow \psi(\ulcorner D \urcorner)$——$D$ 断言关于它自身代码的 $\psi(x)$ 成立。将其应用于 $\psi(x) := \neg\mathrm{Prov}_F(x)$:我们得到一个句子 $G_F$,满足 $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$。通俗地说,$G_F$ 断言"我在 $F$ 中不可证"。

第3步($F \nvdash G_F$)。反证:假设 $F \vdash G_F$。由于 $F$ 是可有效公理化的,这个证明本身有一个代码 $p_0$,所以 $\mathrm{Prf}_F(p_0, \ulcorner G_F \urcorner)$ 为真,从而 $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$(关于具体数字的可证算术事实,其本身在 $F$ 中也可证)。但对角线等价式连同 $F \vdash G_F$ 又给出 $F \vdash \neg \mathrm{Prov}_F(\ulcorner G_F \urcorner)$。于是 $F$ 同时证明了一个命题及其否定,与一致性矛盾。因此 $F \nvdash G_F$。

第4步($G_F$ 为真,并且——假设 $\omega$-一致性——$F \nvdash \neg G_F$)。由于 $F \nvdash G_F$,没有任何数字编码 $G_F$ 的证明,所以 $\neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$ 在 $\mathbb{N}$ 中成立;由对角线等价式,这恰恰就是 $G_F$ 所断言的内容,所以 $G_F$ 为真。如果 $F$ 也能证明 $G_F$ 的否定,即 $F \vdash \neg G_F$,那么把这一点与对角线等价式结合就会得到 $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$——"存在某个 $p$ 编码了 $G_F$ 的证明"——却没有任何实际证明能见证它,而这正是 $\omega$-一致性所排除的情形。所以在 $\omega$-一致性下 $F \nvdash \neg G_F$ 也成立,$F$ 是不完备的。

第一定理的证明——"若 $F$ 一致,则 $F$ 不能证明 $G_F$"——本身可以在 $F$ 内部形式化,从而得到 $F \vdash \mathrm{Con}(F) \to G_F$。如果 $F$ 能证明 $\mathrm{Con}(F)$,用分离规则就会得出 $F \vdash G_F$,与第一定理矛盾。

第1步(可证性谓词不仅可定义,而且可形式化)。由于 $\mathrm{Prov}_F$ 是由可机械检验的关系 $\mathrm{Prf}_F(p,n)$ 构造出来的,以下三条"可导出性条件"本身在 $F$ 内部就是可证的(这正是本论证需要 $F$ 扩展皮亚诺算术、而不仅仅是一致的原因):($P_1$)若 $F$ 证明 $\varphi$,则 $F$ 证明 $\mathrm{Prov}_F(\ulcorner\varphi\urcorner)$;($P_2$)$F$ 证明 $\mathrm{Prov}_F(\ulcorner\varphi\to\psi\urcorner) \to (\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_F(\ulcorner\psi\urcorner))$;($P_3$)$F$ 证明 $\mathrm{Prov}_F(\ulcorner\varphi\urcorner) \to \mathrm{Prov}_F(\ulcorner\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\urcorner)$。

第2步(形式化定理1自身的论证)。由对角线等价式,$F \vdash \neg G_F \to \mathrm{Prov}_F(\ulcorner G_F \urcorner)$。定理1的非形式论证——"如果 $G_F$ 可证,那么它自身的证明就见证了 $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$,而对角线等价式随即又给出 $\neg G_F$ 的一个证明"——除了($P_1$)–($P_3$)所涵盖的机械符号操作外不需要别的东西,因此可以在 $F$ 内部逐步原样模拟为一个形式推导,从而得到 $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \mathrm{Prov}_F(\ulcorner \neg G_F \urcorner)$。由于同时证明了 $G_F$ 及其否定,$F$ 便能通过爆炸原理(ex falso quodlibet)导出 $0 = 1$,这给出 $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \neg\mathrm{Con}(F)$,即 $F \vdash \mathrm{Con}(F) \to G_F$。

第3步(结论)。反证:假设 $F \vdash \mathrm{Con}(F)$。将其与 $F \vdash \mathrm{Con}(F) \to G_F$ 通过分离规则结合,$F$ 就会证明 $G_F$。但定理1已经表明,对一致的 $F$ 有 $F \nvdash G_F$——矛盾。因此 $F$ 无法证明 $\mathrm{Con}(F)$,这正是所要证明的结论。

哥德尔于1929年(在他的博士论文中)证明了这一定理,它说明一阶逻辑的推理规则是完备的:不会遗漏任何逻辑推论。不完备定理(1931年)并不与之矛盾:$G_F$ 不可证,是因为尽管 $G_F$ 在标准模型 $\mathbb{N}$ 中为真,$F$ 却拥有使 $G_F$ 为假的非标准模型。

第1步(可靠性——容易的方向,$T \vdash \varphi$ 蕴含 $T \models \varphi$)。对从 $T$ 到 $\varphi$ 的形式证明的长度作归纳论证。根据定义,$T$ 的每条公理在 $T$ 的任意模型 $M$ 中都为真;每条纯逻辑公理(例如 $\varphi \to (\psi \to \varphi)$)都是有效的,在任何解释下都为真。而每条推理规则都在 $M$ 中保真:对分离规则而言,若 $M \models \theta$ 且 $M \models \theta \to \varphi$,则自动有 $M \models \varphi$。因此证明的每一行都在 $M$ 中为真,特别是最后一行 $\varphi$ 也为真;由于 $M$ 是 $T$ 的任意模型,故 $T \models \varphi$。

第2步(完备性——困难的方向,用逆否命题:$T \nvdash \varphi$ 蕴含 $T \not\models \varphi$)。设 $T \nvdash \varphi$。则集合 $T \cup \{\neg\varphi\}$ 是一致的(若它能推出矛盾,由归谬法 $T$ 就会证明 $\varphi$)。利用亨金方法,将其扩张为一个带见证元的极大一致集 $\Sigma$:每当 $\exists x\, \psi(x)$ 属于 $\Sigma$,就添加一个新常元 $c$ 使得 $\psi(c)$ 也属于 $\Sigma$。构造项模型 $M_\Sigma$,其元素是扩张语言中按 $\Sigma$ 中可证等式加以等同的闭项,关系和函数直接由 $\Sigma$ 解释。对项的长度作归纳(即"真值引理")即可证明,对任意句子 $\theta$ 都有 $M_\Sigma \models \theta \iff \theta \in \Sigma$。

第3步(拼装模型并得出结论)。由于 $\neg\varphi \in \Sigma$,真值引理给出 $M_\Sigma \models \neg\varphi$;又因 $T$ 的每条公理都属于 $\Sigma$,也有 $M_\Sigma \models T$。所以 $M_\Sigma$ 是 $T$ 的一个真实模型,且在其中 $\varphi$ 不成立,即 $T \not\models \varphi$。这就证明了第2步的逆否命题,结合第1步即得:$T \vdash \varphi$ 当且仅当 $T \models \varphi$——这正是哥德尔1929年博士论文的结果,后来由莱昂·亨金(1949年)整理为这里所用的项模型构造。

假设 $H(P, x)$ 能判定停机。构造一台机器 $D(P)$,它先运行 $H(P, P)$,若 $H$ 回答"停机"就永远循环,若 $H$ 回答"循环"就停机。把 $D$ 自己的代码喂给它:$D(D)$ 停机当且仅当 $H(D, D)$ 说它循环——矛盾。这正是哥德尔对角线句子在计算领域的孪生兄弟。

第1步(假设存在一个停机判定器)。反证:假设存在一个算法 $H$,使得 $H(P, x)$ 总是终止,并且正确地回答:若代码为 $P$ 的程序在输入 $x$ 上停机则输出"停机",否则输出"循环"。

第2步(由 $H$ 构造一台对角线机器)。定义一个新算法 $D(P)$,它以程序代码 $P$ 为输入,首先计算 $H(P, P)$——把 $P$ 同时作为程序和输入喂给 $H$ 运行。如果 $H(P, P)$ 回答"停机",那么 $D$ 就故意陷入无限循环;如果 $H(P, P)$ 回答"循环",那么 $D$ 立即停机(比如返回 $0$)。

第3步(把 $D$ 自己的代码喂给它)。由于 $D$ 本身就是一个算法,它自己也有代码,没有什么能阻止我们在这段代码上运行 $D$:考虑 $D(D)$。有两种情形,都不可能成立:如果 $D(D)$ 停机,那么按构造,这恰好发生在 $H(D, D)$ 回答"循环"的时候——也就是说 $H$ 错误地报告 $D$ 在 $D$ 上不停机,而它其实刚刚停机了。反之如果 $D(D)$ 永远运行下去,这恰好发生在 $H(D, D)$ 回答"停机"的时候——也就是说 $H$ 错误地报告它停机,而它其实永远循环。

第4步(结论)。无论哪种情形,$H$ 在输入 $(D, D)$ 上都给出了错误答案,与"$H$ 总是正确"的假设矛盾。所以这样的算法 $H$ 不可能存在:停机问题是不可判定的。