在日常语言里，证明是“说服”。在数学里不是。
一个形式系统由三样东西给定：一套符号与合式公式的规则；一批被无条件接受的公式，叫公理；一批从已有公式生成新公式的规则，叫推理规则。在这个系统里，一个证明是一个有限的公式序列，其中每一条要么是公理，要么由前面若干条按推理规则得到，而最后一条就是被证的那个命题。
这个定义有一个关键性质：证明是可机械检查的。给定一串公式，一台机器可以逐条核对每一步是否合法，不需要理解它在说什么。
正是这个性质使二十世纪初的一个纲领看起来可以实现。
十九世纪末，集合论的悖论动摇了数学的地基。希尔伯特提出的应对方案是：把数学整个形式化，然后用有限的、无争议的手段证明这套形式系统是一致的（不会同时证出一个命题和它的否定），并且是完备的（每个命题要么可证，要么其否定可证）。
如果这个纲领成功，数学就是彻底自我封闭的：一切真理都能在系统内部被抵达，一切怀疑都能在系统内部被消除。
1931 年，哥德尔证明了它不可能成功。
定理（哥德尔，1931）. 设 T 是一个形式系统，满足三个条件： （i）T 的公
理集是递归可枚举的（可以由一台机器逐条列出）； （ii）T 能表示初等算术
（足以谈论自然数的加法与乘法）； （iii）T 是一致的。 则存在一个算术句
子 G，使得 T 既不能证明 G，也不能证明 G 的否定。
三个条件都是实在的，不是修辞。去掉任何一条，结论都不成立——这一点在第九节会展开。
哥德尔的第一件工具是编号：给每个符号一个数，把公式编码成一个数，把证明（公式的有限序列）也编码成一个数。
这一步的意义远大于技术便利。编码之后，“某某是一个合法证明”这样的元数学陈述，变成了关于自然数的一条算术性质。于是一个能谈论自然数的系统，就自动能谈论它自己的语法。
系统获得了谈论自己的能力——这正是条件（ii）的真正内容。它不是“系统要足够复杂”这种模糊的话，而是“系统要强到能把自己的语法编码进去”。
第二件工具是对角化。
对角化引理. 对任何一元公式 φ(x)，存在句子 σ，使得 T ⊢ σ ↔ φ(⌜σ⌝)，其中
⌜σ⌝ 是 σ 自己的哥德尔数。
换成白话：任何一个“性质”，都能造出一个句子，它恰好说“我具有这个性质”。
把 φ(x) 取为“x 在 T 中不可证”，得到句子 G，它说的是：
我在 T 中不可证。
第一半（T ⊬ G）. 假设 T 证明了 G。G 说的是“G 不可证”，而 T 刚刚证明了它——于是 T 证明了一个假的东西。若 T 一致且其可证性谓词忠实，这不可能。故 T ⊬ G。
第二半（T ⊬ ¬G）. 哥德尔原版在这一半用了一个比一致性更强的条件，叫 ω-一致性。1936 年 Rosser 改进了构造（把 G 改成“任何证明我的证明，都有一个更短的证明我的否定的证明”），使得只需简单一致性即可。
这一处细节值得写出来，因为通俗叙述几乎都跳过它，而它恰恰是定理精确形式的一部分。
现在看 G 本身。既然 T ⊬ G，那么 G 所说的“我在 T 中不可证”——是对的。
于是我们站在系统外面，知道 G 为真；而系统内部证不出它。
这是数学史上第一次把“真”与“可证”严格分开。在此之前，两者被默认为同一件事的两种说法。此后，它们是两个概念：真是相对于模型（语义）的，可证是相对于系统（语法）的。
用本书的语言说：S（命题的真）与 D（抵达它的证明路径）不是同一样东西，而E（系统）决定了哪些 D 可用。
定理. 在同样条件下，若 T 一致，则 T 不能证明表达“T 一致”的那个算术句
子 Con(T)。
推论：一个系统的一致性，只能由更强的系统来证。而更强的系统的一致性，又要更强的系统来证。没有终点。
希尔伯特纲领的核心诉求——用系统内部的有限手段确立系统自身的可靠性——至此被否定。
误解一：哥德尔证明了数学是不一致的。 不。定理说的是“若一致，则不完备”。一致性不但没有被否定，反而是定理的前提。
误解二：哥德尔证明了有些真理人类永远无法知道。 不。G 的真我们恰恰知道——第七节就是在系统外面知道的。定理说的是它在那个特定系统内不可证。把 G 加进公理，得到的新系统能证 G；代价是新系统又有新的 G′。
误解三：任何足够复杂的系统都不完备。 不。条件（ii）是“能表示初等算术”，这是一条精确的技术条件，不是“复杂”。有完备且可判定的数学理论：Presburger 算术（只有加法、没有乘法的自然数理论）是完备可判定的；Tarski 证明实闭域理论（因而初等欧氏几何）完备可判定。乘法与加法一起出现，才是那道门槛。
误解四：哥德尔定理适用于物理学、心理学、社会系统、人工智能。 跨域使用之前，必须先证明该领域构成一个满足三条件的形式系统。这一步几乎从来没有人做过。不做这一步而直接套用，是把一条精确的数学定理当成一个比喻。
误解五：哥德尔定理意味着数学真理是相对的。 不。定理分开的是“真”与“可证”，它没有让“真”变得可协商。恰恰相反：G 之所以是一个定理，正因为“G 为真”这件事有一个确定的答案。
三点可以直接对上本编前几章。
其一，命题不能脱离证明路径。 只记录“T ⊢ B”而不记录 D，就看不到证明用了多强的环境，也无法判断这个方法能不能迁移。第一章第四节讲合格路径时，讲的是同一件事的几何版。
其二，环境决定什么能被表达、什么能被证明。 条件（ii）说的正是：环境必须强到能把自己的语法装进去。环境不是背景，它决定表达力的上限。
其三，不完备性是一种 S–D–E 张力。 环境 E 通过路径 D 生成命题 S；当 E 强到能把 D编码为 S 时，自我指涉出现，产生一个在标准意义下为真却不能由 E 内部的 D 抵达的S。升级 E 可以吸收旧缺口，但新系统会生成新的缺口。
两件事常被混为一谈，应当分开。
不完备性（哥德尔）说的是：对满足三条件的任何 T，总存在 T 判定不了的算术句子——这是一条关于全体这类系统的普遍定理。
独立性（Cohen，1963，力迫法）说的是：某个具体的命题（连续统假设）相对于某个具体的系统（ZFC）不可判定。它是对某一句话的具体裁定，靠的是构造两个模型，一个中该命题成立，一个中不成立。
两者的关系是：不完备性保证“这类现象存在”，独立性给出“这一句就是”。方法也完全不同——一个用编码与对角化，一个用模型构造。
先说它不意味着什么：哥德尔定理并不说明本书姊妹卷讨论的那个几何优化猜想不可证。把一切未解决的问题都称为“哥德尔障碍”，是对定理的严重误用。目前没有任何理由把一个具体的几何猜想的困难归因于逻辑独立性。
它给出的是三条方法论要求：
一，把目标命题与已有证明路径分开。 大量数值证据、局部稳定性、晶相排除，仍然不是全局证明。
二，把环境写清楚。 是周期点集，还是任意平稳点过程，还是所有局部有限构型？是欧氏二次失真，还是一般范数？不同的环境对应不同的命题。
三，计算机证书必须公开其形式化范围。 它验证了哪些有限分支、用了什么误差界、遗漏了哪些非周期或大周期情形。一句话概括：哥德尔给出的主要启示不是“猜想可能不可证”，而是“任何证明都必须公开它的系统边界”。
本章讲的是形式系统够不到什么。下一章要问的是另一件事：形式系统本身是被什么发生出来的。