引言：希尔伯特的雄心与一个安静的反击
1900 年八月，巴黎。第二届国际数学家大会上，37 岁的大卫·希尔伯特（David Hilbert）抛出二十三个问题，把数学家未来一百年的航向钉在了讲台上。第二题非常朴素：给数论一个完备且一致的公理系统，并在系统内部证明它自身无矛盾。这听起来像是一个工程师的实事求是——既然几何已经被欧几里得式公理收紧了，那把算术也收紧便是。
1928 年博洛尼亚国际数学家大会上，希尔伯特把这套设想升级为「形式主义计划」（Hilbert programme）：把全部数学翻译成一套有限符号、有限规则的形式语言，证明任何真理都能在系统内被机械地推出。他在闭幕词里说出那句被反复引用的话：「在数学里没有不可知（Wir müssen wissen, wir werden wissen.）」
三年后，1931 年，维也纳一位 25 岁的逻辑学家把一篇题为《论〈数学原理〉及相关系统的形式不可判定命题》的论文交到《数学物理月刊》。文章不长，论证缜密。它说：希尔伯特想要的那种系统，原则上不存在。这位逻辑学家叫库尔特·哥德尔（Kurt Gödel）。
形式系统：让证明像加法一样可机械检验
要看懂哥德尔的反击，先要明白他要打的靶子是什么样的。一个「形式系统」T 由三件东西组成：一套有限的符号、一组语法规则规定哪些符号串算是合法公式、若干公理与若干推理规则规定怎样从公式推出公式。所谓「证明」，就是从公理出发、按推理规则一步步抄下去得到的有限符号串序列。
这套设定的好处是：判定「这一行是否是证明」纯粹是机械活——你不需要懂数学，你只要会比对字符就行。皮亚诺算术（PA, Peano Arithmetic）是这种系统的典型：符号包括 0、后继 S、加法、乘法、相等、若干逻辑联结词与量词，公理涵盖归纳模式与皮亚诺五条。
希尔伯特的赌注是：足够丰富的真理（比如关于自然数的全部真命题）都能被这种纯字符层面的演绎挖出来。「真」与「可证」应当对齐——这是「完备性」（completeness）。同时系统不能既证 \varphi 又证 \lnot\varphi——这是「一致性」（consistency）。
哥德尔的两条定理告诉我们：只要 T 强到足以表达初等算术、并且自洽，这两件事就不可能同时拿到。
第一把钥匙：把公式编码成自然数
哥德尔做的第一件事，今天看来理所当然，在 1931 年却惊心动魄：他让形式系统谈论自身。手段是编码。
每一个符号被分配一个奇素数对应的指数；每一个有限符号串被映为对应素数幂的乘积；每一个证明（公式串的串）也按同样的方法继续向上一层。这套映射通常写作 \#\varphi，称为「哥德尔编号」（Gödel number）。
其中 c(\cdot) 是符号到自然数的字典编码，p_n 是第 n 个素数。算术基本定理保证这种映射是单射——给我一个 \#\varphi，我能唯一地复原 \varphi。
图 1：哥德尔编码把语法层面的对象（公式、证明）单射到自然数。这是让算术「谈论自身」的桥。
关键不仅是「公式有编号」，还在于：「x 是命题 \varphi 在 T 中的一个证明」这件事本身可以被翻译成一个算术谓词 \mathrm{Proof}_T(x, y)，含义是「x 是哥德尔编号为 y 的公式的证明编号」。这个谓词只用加法、乘法、有界量词就能写出来——它本身就是一条 T 内部的合法公式。
由此衍生出「可证性谓词」 \mathrm{Prov}_T(y)，定义为对证明的存在量化：
它的含义是「编号为 y 的公式在 T 中有证明」。哥德尔由此把语法层面的「 T \vdash \varphi 」搬进了算术语言：从外面看是「证明存在」这个元语言事实，从里面看就是一条具体的、可在 T 中讨论真假的算术公式。
第二把钥匙：可表达性引理
仅有编码还不够。哥德尔需要保证：「检查一行字符串是否合法证明」这件机械操作能被算术公式真正表达出来。这一步靠的是可表达性引理（representability lemma）：每一个可计算的（更准确地说：原始递归的）函数与谓词，都能被一条 \Sigma_1 公式在 T 中表达。
这里的 \Sigma_1 公式是指形如 \exists x_1 \cdots \exists x_k\, \phi 的公式，其中 \phi 只用有界量词 (\forall x \le t) 与 (\exists x \le t)。这些公式有一个关键性质叫 \Sigma_1 完备性：
翻译成人话：「确实存在某个具体的自然数见证 σ」这一事实，T 自己有能力按部就班地把这个见证算出来并写下证明。把它套到 \mathrm{Prov}_T(y) 上：检查一串符号是不是合法证明，是有限步字符比对——典型的原始递归操作；因此 \mathrm{Proof}_T 是 \Delta_0 的、 \mathrm{Prov}_T 是 \Sigma_1 的。
由此推出两条以后会反复用到的桥梁性结论。设 \varphi 是任意闭公式：
这是「内化的健全性」：只要 T 真证出了 \varphi，那条具体的证明序列就在标准模型里见证了 \mathrm{Prov}_T(\#\varphi)，再由 \Sigma_1 完备性把它拽回到 T 内部。配合另一条「证出 φ→ψ 推出证出 Prov(φ)→Prov(ψ)」的派生条件 (D2) 与「Prov(φ)→Prov(Prov(φ))」的 (D3)，三条合称 Hilbert–Bernays–Löb 派生条件，将在第二定理里再次出场。
第三把钥匙：对角化引理
有了编码与可表达性，哥德尔做第三件事：让一条公式指向自己。这是对角化引理（diagonal lemma，又称不动点引理）：
构造方法是「对角化」——与康托尔对角线论证同构的技巧。设 \mathrm{sub}(y, n) 表示「把编号为 y 的公式里的自由变量替换为数字记号 \bar n，再返回结果公式的编号」。 \mathrm{sub} 是原始递归的，所以可表达。引入辅助公式：
设 m = \#\theta，把 m 自己代回，得到自指公式：
而按 \mathrm{sub} 的定义， \mathrm{sub}(m, m) 正好就是「把 θ 中自由变量替换成 m」的结果——也就是 \#\varphi 自己。所以 \varphi \leftrightarrow \psi(\#\varphi) 在 T 中成立。整个构造没有任何形而上学，全部是形式系统内的字符替换。
第一不完备性定理：构造那条说自己不可证的句子
把对角化引理套到「 \psi(y) \equiv \lnot \mathrm{Prov}_T(y) 」上，得到一个具体公式 G（哥德尔语句）满足：
由于 \#G 正好就是 G 自身的编号，从外面读 G 说的是：「我在 T 中无法被证明」。下面分两路反证。
方向一： T \vdash G 不可能（只需 T 一致）
反证：假设 T \vdash G。那么这条具体的证明序列见证了「 G 有证明」这个 \Sigma_1 事实，由派生条件 (D1) 把它内化进 T：
而由 G 的等价定义， T \vdash G 又给出 T \vdash \lnot \mathrm{Prov}_T(\#G)。两者并立直接违反 T 的一致性。所以：
方向二： T \vdash \lnot G 不可能（需 \omega-一致）
再反证：假设 T \vdash \lnot G。由 G 的等价定义即得 T \vdash \mathrm{Prov}_T(\#G)，把它展开成存在量化：
另一方面，由方向一已知 T \nvdash G，所以对任何具体自然数 n， n 都不是 G 的证明——再由 \Sigma_1 完备性的反向用法（对 \Pi_1 真句子的可证）：
这就给出了「无穷多条否认」与「一条总存在」并立——正是 \omega-不一致的定义。所以在 T 是 \omega-一致的前提下：
合并两路得到第一不完备性定理：
注意这里 G 在标准模型 \mathbb{N} 中其实是真的——因为它说「我没有证明」，而方向一已经证明它确实没有证明。这就是那句让人毛骨悚然的话：有真而不可证。
Rosser 改进：去掉 \omega-一致
1936 年 Rosser 用一个更巧妙的自指句式抹掉了对 \omega-一致的依赖。他不是构造「我没有证明」，而是构造一个 R，让它说：
这个 R 大致在说「如果有人证出我，那总有更短的反驳」。在仅 T 一致的前提下，同样可推出 T \nvdash R 且 T \nvdash \lnot R。从此第一定理的标准陈述只剩一句话：「足够强的、一致的、可递归公理化的形式系统都不完备」。
图 2：从可证性谓词出发，借不动点引理造出 G；两个方向的反证都通向矛盾，因此 G 与 ¬G 都不可证。
第二不完备性定理：自己证不了自己一致
如果 T 一致，那么至少 \mathrm{Con}(T)（「 T 一致」的形式表达，常写作 \lnot \mathrm{Prov}_T(\#(0=1))）总是真的吧？哥德尔的第二个打击是：这件事 T 自己也证不出来。
证明思路是把第一定理「方向一」的证明全部形式化在 T 内部。那里使用的全部是可被内部复现的推理——只需三条派生条件：
第一定理里「若 T \vdash G 则矛盾」的推理只用了 (D1) 与命题逻辑。把这整段证明逐句内化，会得到一条深刻的形式踪迹：
再由 G 的等价定义 G \leftrightarrow \lnot \mathrm{Prov}_T(\#G) 代入，得到关键一步：
现在反证。如果 T \vdash \mathrm{Con}(T)，由 modus ponens 即得 T \vdash G——与第一定理方向一的结论 T \nvdash G 矛盾。所以 T 证不出 \mathrm{Con}(T)。
这一记打在希尔伯特纲领的命门：他原想用「有限性论证」（finitistic reasoning）证明 PA 一致；如果 PA 真能在自己内部把这件事走完，纲领就成立了。第二定理直接关上了这扇门——任何有意义的一致性证明都必须从外面借更强的系统进来；而那个更强的系统又面对自己的一致性问题。这也正是 Gentzen 1936 年用 \varepsilon_0 序数归纳证明 PA 一致性的代价：他使用了 PA 本身证不出的超限归纳原则。
对角线的家族：从康托尔到哥德尔的统一图景
把对角化引理只当成「证明里的小机巧」会错失故事的全部。它是一族跨越百年的数学武器里最锋利的一把——这族武器有一个共同的名字，叫对角线方法（diagonal argument）。
对角线方法的核心是一句直觉：把一切候选枚举成一张二维表，然后沿对角线翻转每一格，制造出一个无法在表中出现的对象。无论枚举多么完整，新对象都会与第 n 行至少在第 n 位不同——它必然超出枚举的范围。这种「越枚举越溢出」的不变量，是后续每一次不可能性证明共享的母题。
康托尔 1891：连续不可数的原型
对角线方法的起点是康托尔（Georg Cantor）。他要证明 (0,1) 上的实数不可数：假设可数，把它们排成一列十进制小数：
取对角元 a_{nn}，定义新数的第 n 位为 b_n = 5 当 a_{nn} \neq 5 时，否则 b_n = 6，于是：
新数 b 与表中第 n 行至少在第 n 位不同，故不在表中——枚举失败。康托尔由此打开了「无穷有不同等级」的潘多拉之盒，也写下了对角线方法的第一行代码。
罗素 1901、理查德 1905：自然语言里的对角线
罗素悖论是同一道对角线穿上集合论的衣服。考虑「一切不属于自己的集合所组成的集合」：
「集合 ∈ 关系」展成二维表，沿对角线把「∈」翻转为「∉」即得 R，它在表中无处安放。1908 年策梅洛（Zermelo）的公理化集合论正是为了断绝构造 R 的资格而生。
1905 年理查德（Jules Richard）把对角线搬到「自然语言」上：把一切能用有限汉字（或英文）定义的实数排成一列 r_1, r_2, \ldots，再用对角线规则定义新数 d，d 自身也用有限语言被定义了——它应当已在表中，却又不在。这是哥德尔语句的「非形式祖先」：自然语言不够精确以至于产生悖论，但骨架已经成形。哥德尔的成就，就是把理查德式的「应当在却不在」从自然语言挪到形式系统，让悖论变成定理。
图灵 1936：可计算性意义上的对角线
图灵（Alan Turing）把对角线搬到了「程序」上。枚举所有图灵机 M_1, M_2, M_3, \ldots，假设存在能判定停机的总函数 H(i, j) \in \{0, 1\}。构造一台新机器：
D 自身是某台 M_d。问 D(d) 是否停机：若 H 说「停机」则 D 死循环，若 H 说「不停机」则 D 停机——两种情况都与 H 的判断矛盾。这是计算意义上的对角线：第 i 行（第 i 台机器）第 i 列（输入自身编号）上的判定结果被翻转，新对象无处藏身。
图灵 1936 与哥德尔 1931 是同一道闪电的两次显现。把「图灵机 M 在输入 x 上停机」翻译为算术公式 \mathrm{Halt}(M, x)：若 PA 完备，对每个 (M, x) 它必证 \mathrm{Halt} 或 \lnot \mathrm{Halt}，于是枚举 PA 的所有证明就成了停机判定算法——与图灵不可判定性矛盾。反向也成立：哥德尔语句直接给出一个不可判定的算术问题，构成图灵结果的非构造性证明。同一根铁链，从证明面与计算面都封死了形式化的极限。
Tarski 1936：真理不可在内部定义
同一年，Tarski（Alfred Tarski）证明了「真理不可定义性定理」（undefinability of truth）：在足够丰富的算术语言里不存在一个公式 \mathrm{True}(y) 使得对任何闭公式 \varphi：
证明又是对角线：把对角化引理用在 \lnot \mathrm{True}(y) 上，得到自指句 L \leftrightarrow \lnot \mathrm{True}(\#L)——这是说谎者悖论的形式化版本。若 True 存在，则 L 真当且仅当 L 假，矛盾。所以 True 不可在算术内部表达。
Tarski 与哥德尔的对照意味深长：「可证」可以在系统内被算术地定义，「真」却不行。这正是哥德尔语句必须用「不可证」（而非「不真」）来自指的根本原因——前者写得出来，后者写不出来。
Lawvere 1969：所有对角线证明的母定理
1969 年，范畴论家 Lawvere（William Lawvere）发表 Diagonal arguments and cartesian closed categories，给出统一所有对角线论证的母定理。其核心是一句话：
把它逆否过来就是所有不可能性结果的统一形式：若某个 f: Y \to Y 没有不动点（即「翻转」总能逃脱），则 A \to Y^A 不可能有点状满射。
把表格列出来比例对照：
每一栏都是同一个 Lawvere 不动点的不同投影。在哥德尔语境里，\mathrm{sub} 函数提供了那个「点状满射」——它把每一条带自由变量的公式与一个具体的自指句对应；只要某个 \psi 像 \lnot \mathrm{Prov}_T 那样在逻辑层面无不动点，对角化引理立刻造出哥德尔句 G。这就是对角化引理的「形而上原因」。
为什么哥德尔不完备必须靠对角线
现在可以正面回答：为什么对角线方法必然导出哥德尔不完备？
哥德尔讨论的是「形式系统的表达能力」与「形式系统的证明能力」之间的裂缝。对角线是探测裂缝的唯一通用工具。一旦表达系统强到能描述「自身的某个属性」（这是可表达性引理），它就在事实上构造了一张「自身索引表」；只要表中的属性允许逻辑取反（例如 \lnot \mathrm{Prov}_T 是 \mathrm{Prov}_T 的合法翻转），对角线立刻造出表达系统无法吞下的句子。
这条逻辑链条不依赖任何具体编码。把哥德尔编号换成 ASCII、UTF-8、Lisp S-表达式、λ 演算的 Church 数——只要它能编码自身语法，对角线就在那里。这也解释了为什么类似论证可以在表达系统中无限蔓延：Löb 定理、Rice 定理、Curry 悖论、Berry 悖论、Yablo 悖论、Y 组合子、不动点组合子——每一个都在重演「枚举 + 翻转」的两步骨架。
所以哥德尔不是用了「一个聪明的小技巧」。他是把康托尔为「连续 vs. 可数」准备的武器，转手对准了「真 vs. 可证」。形式系统拥有自我指涉的能力，是它的力量；正因为这份力量，它不得不留下一道无法弥合的裂缝——那条裂缝就是对角线，而哥德尔语句只是这道裂缝在算术语言里的一个具体名字。
图 3：六条独立的不可能性结果其实是同一个 Lawvere 不动点定理沿不同范畴的投影。哥德尔不完备性是这族对角线武器在「形式算术」上的精确落点。
为什么「含初等算术」就足以引爆自我指涉
读到这里，多数读者心里其实积着一个更尖锐的问题：自指句 G 听上去像哲学家的玩具——凭什么 PA 这样一个研究加法乘法的朴素系统，就一定能造出「我说自己不可证」这样一个闭环？哥德尔的回答简洁得近乎冷酷：因为乘法已经够了。下面把这条回答拆成五步。
反例先行：只有加法的算术其实是完备且可判定的
1929 年，Presburger（Mojżesz Presburger）证明了 Presburger 算术（只含 0, S, +, = 与一阶量词的理论）是完备、一致、可判定的——存在算法能在有限时间内判断它的任一闭公式真假。同年 Skolem 也证明了「只有乘法」的 Skolem 算术同样可判定。
区别只有一件事：×。把乘法删掉，哥德尔的整台机器立刻拆散。这不是偶然——它告诉我们「含初等算术」这四个字，真正分量在于加法乘法同时存在。
算术基本定理：乘法为编码送来唯一性
哥德尔编号长这样：
这个表达式之所以是单射，完全依赖算术基本定理：每个正整数有唯一素因子分解。算术基本定理是关于乘法的事实，不是关于加法的。在 Presburger 算术里，「素数」这个概念都写不出来——把 p 是素数翻译成只用加法的公式是不可能的，更别说分解。
失去乘法 → 失去唯一编码 → 失去把语法压回算术的桥梁。Presburger 算术的「内部世界」太干净，干净到无法谈论自身。
β-函数引理：原始递归全部进入算术
哥德尔在 1931 年的原文里独立证明了一条关键技术杠杆——β-函数引理：存在一个仅用加法乘法定义的算术函数 \beta(c, d, i)，对任意有限序列 a_0, a_1, \ldots, a_n 都能找到 c, d 使：
它的实现用到中国剩余定理：把无穷长的「序列」压进两个自然数 (c, d)，再用「除 1 + (i+1)d 的余数」把第 i 个分量取出来。整个构造只用加法、乘法、有界量化。
β-函数引理立刻推出一句重磅断言：所有原始递归函数都可在 PA 中表达。一旦这条桥架起来，多米诺骨牌就开始倒：
注意：\mathrm{Prov}_T(y) 不是哥德尔从外面塞进 PA 的；它是 PA 自己用加法乘法从内部写出来的一条具体合法公式。系统拥有了「谈论自身可证性」的语言能力。
对角化引理的启动条件低得惊人
回头看对角化引理需要什么前提：
仔细审视证明，它真正用到的只有两件事：
编码函数 \# 单射
（由乘法 + 算术基本定理给出）
替换函数 \mathrm{sub}(y, n) 可表达
（由 β-函数引理 + 原始递归给出）
两条加起来，就是「初等算术」三个字的全部分量。不需要选择公理，不需要无穷集合论，不需要二阶逻辑，不需要归纳模式的全部强度——只需要小学算术。这就是为什么哥德尔不完备性的下界低得吓人：任何能写出「乘法表」的一阶系统都已经站在自指的悬崖边。
含初等算术 ⟹ 内置一台简易解释器
把上面四步压成一句话：「含初等算术」=「内部隐藏着一台能解释自身语法的计算机」。
这台解释器有以下能力：把每条公式当字符串处理（编码）、能取自身的字符串表示（哥德尔数）、能做替换（sub）。Lawvere 母定理告诉我们：只要某个范畴拥有「自身索引能力」（点状满射 A \to Y^A），它就把一切「逻辑层面无不动点」的内态射变成对角线证据。在 PA 里，「自身索引能力」由 \mathrm{sub} 提供，「无不动点的内态射」由否定 \lnot 与可证性谓词 \mathrm{Prov}_T 的组合提供——两件事一拼，G \leftrightarrow \lnot \mathrm{Prov}_T(\#G) 立刻自动落地，根本无需作者的灵感乍现。
换句话说：哥德尔语句不是天才偶然造出的怪物，而是「会算乘法的形式系统」必然吐出的副产物。
一张权力光谱
把常见形式系统按「乘法 / 自指 / 完备 / 可判定」做横向对照：
最值得驻足的是 Robinson 算术 Q：只有 7 条极弱的公理，连数学归纳模式都没有，但哥德尔不完备性已经在它身上成立。这说明哥德尔的下界其实远比 PA 还低：不需要归纳法，只需要「能算乘法表」的程度，自指就栖身其中。希尔伯特原本期待用比 PA 更弱的「有限性论证」（finitistic reasoning）证明 PA 一致——而 Q 已经不完备的事实，等于把这条退路也封死。
边界的哲学含义
所以哥德尔结果真正的震撼力，不在于他造了一条偷天换日的奇怪句子，而在于他证明了：「算术」与「自我指涉」是一对孪生儿。一个形式系统只要算得出乘法表，它就必然具备指向自身的能力，也必然承担起这份能力带来的不完备代价。中间没有可以躲藏的安全地带。
希尔伯特纲领的真正破灭点也在这里：他想要的「足够丰富又完全自洽」的系统，在算术意义上是空集。要么放弃乘法（像 Presburger 算术那样，可判定但弱到无法表达数论的核心命题），要么接受不完备。中间路线被定理彻底关闭。这才是「形式系统的边界」最锋利的那条切线。
结语：边界并不是失败
哥德尔之后，许多人误读他：以为他证明了「数学有真不能被知道」，因此理性的事业蒙尘。这是把第一定理当成形而上学的悲剧。哥德尔本人不这样看。他证明的是：任何单一的、足够强的形式系统都不完备；但它没有说真理本身是模糊的，也没有说人不能通过升级系统、构造新公理（比如大基数公理）逐步逼近更广阔的真理。
这甚至给了数学一种意外的开放性。形式系统不再被想象成一座最终封顶的金字塔；它更像是一种递归的、永远向上的脚手架——你以为爬到了顶，往上看，还有一层属于「这层之外」的真理等着新的公理与新的视角。希尔伯特说「我们必须知道，我们将要知道」；哥德尔的回答是「知道的方式不止一种，而且永不收尾」。
真正的悲剧反倒落在那位比哥德尔还更早把同样思路嗅出端倪的人身上——亚兰·图灵在三十四岁时把生命交给了一杯氰化物的苹果。但他留下的「机械证明」与哥德尔留下的「自我指涉」一同打开了一扇门：在这扇门里，「证明」与「计算」开始不再是两件事。
与下章纽带
哥德尔的不动点引理与图灵的对角线在结构上对偶，已经在暗示一种更深的统一：证明就是某种程序。下一章我们将走进柯里-霍华德同构（Curry–Howard correspondence）——把命题翻译成类型、把证明翻译成 λ 项、把推理规则翻译成函数构造。在那里，写一个数学证明和写一段计算机程序变成了同一件事；而本章里那些可证、可判定、可计算的边界，会在新的语言里重新登场。