对角引理 | Codeboy's Blog

形式陈述

设 $A(z)$ 是算术语言的公式，其自由变量至多为 $z$ 。固定语法编码， $\operatorname{code}(\varphi)$ 表示元语言中的自然数代码， $\overline n=S^n0$ 表示对象语言数码。对角引理断言：可构造一个句子 $G$ ，使

\mathrm{PA}\vdash G\leftrightarrow A\bigl(\overline{\operatorname{code}(G)}\bigr).

任何扩张 PA 的理论也证明该等价。事实上，证明只需基本一阶等号逻辑，以及下述对角代入函数的逐输入唯一图表示；因此结论也可在满足这些条件的更弱理论中成立。引理本身不要求理论一致。对 Robinson 算术 $Q$ ，原始递归函数也有逐输入唯一图表示，所以同一构造给出 $Q$ 版本；这是后续 Rosser 证明使用的接口，不能把 PA 版本的归纳证明本身当作 $Q$ 的证明。

这里得到的是可证等价，不是两个公式具有相同字符串，也不是两个代码数值相等。句子 $G$ 的文字无需出现“我”，它的有限语法构造足以保证这个等价式。

直觉

先做一个带空位的模板，再把模板自己的编号作为数码填进空位。填进去的是模板编号；模板中的算术公式负责把它转换成填好以后整句话的编号。这样可避免“必须先知道最终句子才能写出最终句子”的循环。

模板、代码与数码代入的关系；模板代码 b 经对角化得到最终代码 g，理论内证明连接 G 与 A 的数码实例

图中编码和代入在元语言中完成；底部双向箭头是 PA 内的可证等价。 $b$ 和 $g$ 分别记录模板与完成句的代码。

例子与边界

四个对象的构造账本

用 $x=v_0$ 作指定输入变量。设 $d(a)$ 将代码为 $a$ 、自由变量至多为 $x$ 的公式中的自由 $x$ 替换为 $\overline a$ ，返回新公式代码；不合条件的输入返回固定默认值。该总函数原始递归，因此存在公式 $D(x,y)$ ，当标准数 $d(n)=m$ 时，PA 证明

D(\overline n,\overline m),\qquad \forall y(D(\overline n,y)\to y=\overline m).

$d$ 是元语言中的计算函数，算术语言通过关系公式 $D$ 表示这项计算。

将 $A$ 和 $D$ 内部的绑定变量适当改名，取不引起捕获的 $y$ ，按次序定义

\begin{aligned} B(x)&:=\exists y\bigl(D(x,y)\land A(y)\bigr),\\ b&:=\operatorname{code}(B(x)),\\ G&:=B(\overline b),\\ g&:=\operatorname{code}(G). \end{aligned}

$A(y)$ 表示把 $A(z)$ 的自由 $z$ 无捕获地替换为 $y$ 。 $B$ 自由变量至多为 $x$ ，所以 $G$ 是句子。逐行检查定义可得元语言等式 $d(b)=g$ ： $d$ 对模板代码所执行的，恰好就是第三行的代入操作。

双向等价的完整证明

由 $D$ 的表示性质，首先得到两个 PA 定理：

D(\overline b,\overline g),\tag{1}

\forall y\bigl(D(\overline b,y)\to y=\overline g\bigr).\tag{2}

接下来全部在 PA 内推导。假设 $G$ ，按其定义有

\exists y\bigl(D(\overline b,y)\land A(y)\bigr).

取存在见证 $y$ 。由式 (2) 得 $y=\overline g$ ，再对 $A(y)$ 使用等号替换，得到 $A(\overline g)$ 。消去存在见证并解除假设，便有 $\mathrm{PA}\vdash G\to A(\overline g)$ 。这里逐输入唯一性的作用是确定任意存在见证 $y$ ，包括非标准模型中的见证。

反方向假设 $A(\overline g)$ 。将它与式 (1) 合取，再以闭项 $\overline g$ 作存在见证，得

\exists y\bigl(D(\overline b,y)\land A(y)\bigr),

这按定义就是 $G$ 。因此 $\mathrm{PA}\vdash A(\overline g)\to G$ 。合并两方向并使用外部记号 $g=\operatorname{code}(G)$ ，得到引理所述等价。这一方向只用具体值实例，不需要唯一性。

整个证明只用了输入 $b$ 对应的值实例与唯一性，因而无需 $D$ 的统一总性定理。 $b,g$ 的十进制值取决于 $D$ 的具体公式文本；这里用定义精确追踪两者即可。

推论与应用

令 $A(z)=\neg\operatorname{Prov}_T(z)$ ，其中 $\operatorname{Prov}_T$ 是适当编码的可证明性公式，便得到

T\vdash G\leftrightarrow\neg\operatorname{Prov}_T\bigl(\overline{\operatorname{code}(G)}\bigr)

（此处取 $T$ 为 PA 的扩张）。这只是第一不完备定理的自指构造环节；从该等价走到不可证与不可否证，还要检查证明谓词及相应一致性或可靠性假设，Rosser 形式则使用另一种比较证明的公式，并用固定数码的有限排除完成两向反证。第二不完备定理进一步列出 HBL 三条件，用两次内部证明组合和一次可证明性内省，逐步推出 $\operatorname{Con}(T)\to G$ 。

它与Kleene 递归定理共享“模板接收自己的描述”这一构造思路，但结论类型不同。Kleene 定理给出程序索引 $e$ 与变换后索引 $f(e)$ 所计算的偏函数外延相等；这里给出理论内的公式可证等价。两种固定点分别比较程序行为和逻辑公式，而非代码数值。

验收练习。 对任意给定的 $A(z)$ 写出 $B,b,G,g$ ，解释 $d(b)=g$ ，并在双向证明中标出式 (1)、(2) 的不同用途。若取 $A(z)$ 为恒真公式 $z=z$ ，所构造的 $G$ 可在 PA 中证明；这说明固定点并不自动成为不可判定句。若取不可证明性公式，仍需返回第一不完备定理核对下一步假设。

参考资料

Open Logic Project，The Open Logic Text: Incompleteness，rev. 9620cc7，2026-07-12，§5.2，Lemma 5.2，印刷62–63页：关系表示与存在量词构造、两方向证明。
Peter Smith，An Introduction to Gödel’s Theorems，corrected second edition，§24.4，Theorem 24.4，印刷179–180页：对角引理及存在量词版本的构造。

形式陈述 ​

四个对象的构造账本 ​

双向等价的完整证明 ​

反向链接

形式陈述

四个对象的构造账本

双向等价的完整证明