Gödel 第二不完备定理

形式陈述

设 $T$ 是经典一阶算术理论，递归可公理化并扩张 PA。固定标准的证明编码及其可证明性公式 $\operatorname{Pr}_T(x)$ ；下面明确列出证明需要的三个可导出条件。记

\Box A\;:=\;\operatorname{Pr}_T\bigl( \overline{\operatorname{code}(A)}\bigr),\qquad \bot\;:=\;(0=1),\qquad \operatorname{Con}(T)\;:=\;\neg\Box\bot.

$\Box$ 是元语言缩写，不是给算术语言新添的模态算子。每次使用都先把整句 $A$ 编码，再把代码写成数码。 $T$ 证明 $0\ne1$ ，因此 $\bot$ 在推导中可充当矛盾。

Hilbert–Bernays–Löb 可导出条件如下，对任意句子 $A,B$ ：

T\vdash A\quad\Longrightarrow\quad T\vdash\Box A; \tag{D1}

T\vdash\Box(A\to B)\to(\Box A\to\Box B); \tag{D2}

T\vdash\Box A\to\Box\Box A. \tag{D3}

(D1) 是关于 $T$ 定理的外部规则；(D2)、(D3) 是 $T$ 可证明的内部公式模式。它们分别对应具体证明可编码、证明可以按 modus ponens 组合、理论能验证“存在一份证明”本身具有证明。

Gödel 第二不完备定理断言：如果 $T$ 一致，且所选 $\operatorname{Pr}_T$ 满足这些条件，则

T\nvdash\operatorname{Con}(T).

标准的 PA 证明谓词满足三条件；对有效公理扩张，使用规范的公理枚举与证明编码建立相应条件。本文从三条件出发完成内部推导，条件对具体编码的验证见参考资料。仅在标准自然数中表达同一个可证集合，不自动保证所选公式满足内部的 (D2)、(D3)。

直觉

理论可以把“没有任何有限证明推出 $0=1$ ”写成一个算术句子。困难在于用自己的证明规则证明这个无界断言。对角化构造 $G$ ，使它可证等价于 $\neg\Box G$ ；三条件则让理论在内部证明：如果存在 $G$ 的证明，就存在矛盾的证明。因此，一致性公式蕴涵 $G$ 。

由可导出条件把一份G的可证明性分成两条内部推导，合并为矛盾的可证明性，再得到一致性蕴涵G

图中两条分支是 $T$ 内由 $\Box G$ 推出的结论，合取后共同供第二次 (D2) 使用；底部先反置再使用固定点等价。外部的一致性假设只在最后排除 $T$ 真的证明 $G$ 或 $\operatorname{Con}(T)$ ，不参与这张内部推导图的建立。

例子与边界

固定点与两次不同的证明组合

由对角引理，取句子 $G$ 满足

T\vdash G\leftrightarrow\neg\Box G.\tag{1}

先用正方向及 $T\vdash\neg\bot$ 得到定理

T\vdash G\to(\Box G\to\bot).\tag{2}

(D1) 作用于这条已经证明的整句，给出

T\vdash\Box\bigl(G\to(\Box G\to\bot)\bigr).\tag{3}

第一次使用 (D2)，代入 $A=G$ 、 $B=(\Box G\to\bot)$ ，再与式 (3) 作 modus ponens，得到

T\vdash\Box G\to\Box(\Box G\to\bot).\tag{4}

第二次使用 (D2)，这次代入 $A=\Box G$ 、 $B=\bot$ ：

T\vdash\Box(\Box G\to\bot) \to(\Box\Box G\to\Box\bot).\tag{5}

式 (4)、(5) 只差一个输入 $\Box\Box G$ 。由 (D3) 补上它：

T\vdash\Box G\to\Box\Box G.\tag{6}

于是可在 $T$ 内暂时假设 $\Box G$ ：式 (4) 给 $\Box(\Box G\to\bot)$ ，式 (6) 给 $\Box\Box G$ ，式 (5) 合并两者得到 $\Box\bot$ 。解除假设，便有

T\vdash\Box G\to\Box\bot.\tag{7}

反置式 (7)，再用式 (1) 的反方向 $\neg\Box G\to G$ ，得到

T\vdash\neg\Box\bot\to\neg\Box G, \qquad \boxed{T\vdash\operatorname{Con}(T)\to G}.\tag{8}

至此没有使用外部一致性。所有 box 都来自 (D1) 对定理的应用，或来自已列出的内部条件；没有给一个临时假设直接加 box。

外部一致性完成最后的反证

现在才假设 $T$ 一致。若 $T\vdash G$ ，(D1) 给出 $T\vdash\Box G$ ，式 (1) 又给出 $T\vdash\neg\Box G$ ，矛盾。因此 $T\nvdash G$ 。

若进一步反设 $T\vdash\operatorname{Con}(T)$ ，式 (8) 立即推出 $T\vdash G$ ，与刚得到的结论冲突。所以 $T\nvdash\operatorname{Con}(T)$ 。这里仅用原始 Gödel 句的不可证方向；不需要 $T\nvdash\neg G$ ，也不需要 $\omega$ -一致性或所有定理为真的可靠性假设。Rosser 的第一定理解决普通一致性下的双向不可证，它使用另一种证明比较公式，不能直接替换这里已满足 HBL 条件的标准谓词。

两层 box 与有限一致性实例

为核对句码层次，设

g=\operatorname{code}(G),\qquad h=\operatorname{code}\bigl(\operatorname{Pr}_T(\overline g)\bigr).

则 $\Box G$ 展开为 $\operatorname{Pr}_T(\overline g)$ ，而 $\Box\Box G$ 展开为 $\operatorname{Pr}_T(\overline h)$ 。后者的参数是整句“ $G$ 可证”的代码，不是再次填入 $g$ 。同样，式 (3) 编码整个蕴涵句；式 (4) 右端编码的是 $\Box G\to\bot$ 。

(D1) 也不表示 $T\vdash A\to\Box A$ 。前者要求先有一份无临时假设的 $A$ 的证明；后者允许在内部假设 $A$ 后直接得到可证明性，是不同的断言。它更不允许反射规则 $\Box A\to A$ ；例如取 $A=\bot$ ，这个内部实例已等价于 $\operatorname{Con}(T)$ ，正是定理排除的目标。

另一个可逐项核验的例子是有限一致性。若 PA 一致，对每个外部固定 $n$ ， $0,\ldots,n$ 都不是 $0=1$ 的证明代码。逐个计算、用数码表示和有限枚举合并，PA 可以证明

\forall p\left(p\le\overline n\to \neg\operatorname{Proof}_{\mathrm{PA}} (p,\overline{\operatorname{code}(0=1)})\right).

每个 $n$ 对应一份有限 PA 证明，不能把这无限多份证明合并为一个关于所有 $n$ 的内部全称证明。若能完成这种统一化，就会得到 $\operatorname{Con}(\mathrm{PA})$ ，而第二定理恰好排除它。

推论与应用

若 PA 一致，它不能证明自身的标准一致性公式；ZFC 则可构造自然数模型并证明 PA 一致性。这是相对一致性工作的典型方向：证明被移到更强的理论中。对 ZFC 自身，也可把其有效形式系统的证明编码成自然数；在对应的算术解释和标准可导出条件下，同一论证限制其证明自身一致性。

不一致的理论可以证明所有句子，包括自己的“一致性”公式，所以外部一致性条件不能删除。对极弱理论或非标准的可证明性表示，则应逐条核对固定点构造和 HBL 条件，不能只凭一个公式被命名为 $\operatorname{Pr}$ 就应用结论。

这也解释了证明论为何研究相对一致性与序数分析：更强的元理论或良基归纳原则可以为较弱理论建立无法在其内部完成的统一保证。第二定理限定的是指定系统、指定标准证明表达下的内部自证，不否定外部一致性研究。

验收练习。 不看式 (4)、(5)，写出两次 (D2) 的 $A,B$ ，标出 (D3) 补上的输入；再说明式 (8) 与最终不可证结论分别是否使用了一致性。最后展开 $\Box\Box G$ 的数码，检查没有把 $g$ 与 $h$ 混同。

参考资料

Open Logic Project，The Open Logic Text: Incompleteness，rev. 9620cc7，§§5.6–5.7，Theorems 5.8–5.9：三条件及式 (5.5)–(5.13) 的内部推导。
Peter Smith，An Introduction to Gödel’s Theorems，corrected second edition，§§33.1–33.2、35.1–35.3，印刷245–248、258–261页：box 缩写、可导出条件及规范证明谓词的验证。本文 D1–D3 编号指三条件，与该书局部固定点方向的编号分开。

形式陈述 ​

固定点与两次不同的证明组合 ​

外部一致性完成最后的反证 ​

两层 box 与有限一致性实例 ​

反向链接

形式陈述

固定点与两次不同的证明组合

外部一致性完成最后的反证

两层 box 与有限一致性实例