第3卷第10章哥德尔不完备定理

沿希尔伯特计划、形式系统P、哥德尔数、原始递归与表现定理、可证明性算术化、对角化五季路线，重建第一和第二不完备定理的条件、证明结构与建设性意义。

学习目标

能区分形式系统的相容性、完备性与可有效公理化条件，并解释形式证明为何可以机械检查
能把公式、证明和“可证明性”编码为自然数，说明哥德尔数与原始递归函数各自承担的角色
能沿表现定理与对角化构造g，跟踪第一不完备定理两半证明的条件差异
能区分“系统不能证明自身相容”与“系统有矛盾”，并用交互实验复查形式世界与含义世界的边界

从一整天的路线图开始

春假里，“我”、尤里与泰朵拉来到双仓博士的私立图书馆，在名为“氯”的会议室与米尔嘉会合。今天的任务不是背一句“存在不可证明的真理”，而是完整走完“用数学研究数学”的路线。

先预测四个问题，再在章末逐项复查：

若一个系统没有矛盾，它是否一定能判定每个语句？
一个给定符号串是不是正确证明，为什么可以机械检查？
公式怎样在不使用自然语言引号的情况下谈论自身？
“系统不能证明自己相容”是否等于“系统其实有矛盾”？

10.1 双仓图书馆

10.1.1 入口

双仓图书馆位于山坡，收藏大量数理书籍，也有供讨论和小型研究会使用的房间。三人按指引找到一楼的Chlorine房间。空间从普通图书馆切换成研究会议室，预告本章也会不断在日常语言、元数学与形式系统之间切换。

10.1.2 氯

米尔嘉列出整天的大纲：

希尔伯特计划为何要给数学建立形式化基础；
哥德尔两条不完备定理究竟说什么；
逐步研究第一定理的证明；
讨论不完备定理的建设性意义。

她把证明分成春天、夏天、秋天、冬天与新春。季节不是装饰，而是依赖顺序：后一步只能使用前一步已经构造好的对象。

10.2 希尔伯特计划

10.2.1 希尔伯特

希尔伯特希望给数学建立牢固基础，原章把计划拆成三步：

导入：用形式系统表示数学；
证明相容性：不能同时证明A与¬A；
证明完备性：每个语句都能由A或¬A的一方判定。

写成可证性记号：

\operatorname{Con}(T) \quad\Longleftrightarrow\quad \nexists A\, \bigl(T\vdash A\land T\vdash\neg A\bigr),

\operatorname{Complete}(T) \quad\Longleftrightarrow\quad \forall A\, \bigl(T\vdash A\lor T\vdash\neg A\bigr).

这里的T⊢A是系统内部的语法性质，不等于“我们觉得A有道理”。

10.2.2 猜谜

形式证明是有限序列：

a_1,a_2,\ldots,a_n

要求每个a_i是公理，或由更早的公式按推理规则得到；末行a_n称为定理。

这立刻回答三个原章谜题：

单独由公理a组成的长度1序列就是形式证明，所以每个公理也是定理。
若完备系统X中a不可证，则¬a必可证；把a追加为新公理后，新系统同时证明a与¬a，因此矛盾。
矛盾系统能证明所有公式，所以它在上述技术定义下反而是完备的。

词语的日常褒贬不能代替定义。“完备”不自动包含“相容”。

10.3 哥德尔不完备定理

10.3.1 哥德尔

哥德尔在1931年的论文《论〈数学原理〉及其相关系统的形式不可判定命题（I）》中证明了两条著名定理。

第一不完备定理的现代概括是：对相容、能够表达足够自然数算术且可有效公理化的形式系统T，存在语句G_T，使系统无法完成对它的判定。在原章采用的证明版本中：

T\nvdash G_T, \qquad T\nvdash\neg G_T.

证明G_T不可证只需相容性；原论文处理¬G_T不可证时使用更强的ω相容性，后来罗赛尔技巧把相应条件减弱到相容性。

第二不完备定理说，在适当条件下，若T相容，则：

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

也就是T不能在自身内部证明那个准确表达“T相容”的算术语句。

10.3.2 讨论

结论不是“数学含有矛盾”。它谈的是满足具体条件的，而且“不能证明自身相容”与“自身不相容”逻辑上完全不同。

若要证明某个系统的相容性，可以在更强的元系统中进行。第二定理限制的是系统对自身的证明，不禁止系统研究其他系统，也不禁止数学家做相对相容性证明。

同样，“不完备定理证明了理性的界限”不是定理内容。方程x^2=-1无实数解只说明实数域中的性质，不是理性失败；不完备定理也只精确说明形式系统的性质。

10.3.3 证明的概要

五个阶段是：

\text{春：形式系统P} \longrightarrow \text{夏：哥德尔数} \longrightarrow \text{秋：原始递归与表现定理}

\longrightarrow \text{冬：把证明关系算术化} \longrightarrow \text{新春：构造不可判定语句}.

缺少任一环都无法闭合：没有P就没有被研究对象；没有编码就不能用数论谈公式；没有表现定理就不能把元数学谓词送回系统；没有证明谓词就不能让语句谈论“可证”。

10.4 春天：形式系统P

10.4.1 基本符号

形式系统P在《数学原理》的类型系统上加入皮亚诺算术等公理。七个常量是：

0,\ f,\ \neg,\ \lor,\ \forall,\ (,\ ).

f表示后继。变量按类型分层：

x_1,y_1,z_1,\ldots

表示数；

x_2,y_2,z_2,\ldots

表示数的集合；更高型继续表示低一型对象的集合。类型差一是避免罗素式自我成员关系的重要护栏。

10.4.2 数项和符号

自然数由数项表示：

\overline0=0,\quad \overline1=f0,\quad \overline2=ff0,\quad \overline n=f^n0.

第一型符号还包括对第一型变量反复应用f得到的串；第n型变量本身是第n型符号。

10.4.3 逻辑公式

基本逻辑公式形如：

a(b),

其中a比b高一型。合式公式由递归语法生成：

基本逻辑公式是公式；
若a是公式，则¬(a)是公式；
若a,b是公式，则(a)∨(b)是公式；
若a是公式且x为变量，则∀x(a)是公式；
只有按以上有限步骤得到的串才是公式。

蕴含、合取、等价和存在量词只是省略：

a\to b:=\neg a\lor b,

a\land b:=\neg(\neg a\lor\neg b),

a\leftrightarrow b:=(a\to b)\land(b\to a),

\exists x\,a:=\neg\forall x\,\neg a.

10.4.4 公理

公理分成五族：

公理族	作用	代表内容
I	皮亚诺算术	`fx≠0`、后继单射、归纳
II	命题逻辑	关于`∨`与`→`的四个模式
III	谓词逻辑	全称实例化与量词移动
IV	集合内涵	公式决定相应集合
V	集合外延	元素相同则集合相同，并允许形式提升

系统用：

x=y \quad:\Longleftrightarrow\quad \forall u\,(u(x)\to u(y))

表达等号。公理III-1中的：

\operatorname{subst}(a,v,c)

表示把公式a中所有自由的v用同型符号c安全代换，不能造成变量捕获。

10.4.5 推理规则

规则一是假言推理：

\frac{a\qquad a\to b}{b}.

规则二是全称化：

\frac{a}{\forall v\,a},

前提是a已在无额外假设下推出。至此P的符号、公式、公理、规则和形式证明都已封闭定义。

Form System Pipeline：证明不是直觉上的说明，而是每一行都能检查的有限对象。

10.5 午饭时间

10.5.1 元数学

一行人转到名为“Oxygen”的房间午餐。米尔嘉说明，若要严谨讨论“某证明不可能存在”，必须先把“公式”“证明”“不可能存在”都对象化。以数学方法研究形式化数学，称为。

这与ε-δ语言类似：精确定义出现后，原本模糊的“趋近”才能成为数学对象。

10.5.2 用数学研究数学

把不完备定理改写成人生格言可以是个人联想，却不是数学证明。原章持续要求把“数学层面的结论”与“从结论获得的启示”分开。

10.5.3 苏醒

午饭后“我”短暂睡着。泰朵拉谈到从米尔嘉与学长身上学到的不只是解题技巧，还有“乐在其中并认真面对、追求真正理解”的态度。醒来后，夏天开始。

10.6 夏天：哥德尔数

10.6.1 基本符号的哥德尔数

先编码基本符号。常量取不大于13的奇数；这一步开始使用：

\begin{array}{c|ccccccc} \text{符号}&0&f&\neg&\lor&\forall&(&)\\ \hline \text{编码}&1&3&5&7&9&11&13 \end{array}

大于13的质数编码第一型变量：

x_1\mapsto17,\quad y_1\mapsto19,\quad z_1\mapsto23,\ldots

第n型变量取对应质数的n次幂：

x_n\mapsto17^n,\quad y_n\mapsto19^n,\ldots

由素因数分解即可恢复变量基名与类型。

10.6.2 序列的哥德尔数

有限序列：

(n_1,n_2,\ldots,n_k)

编码为：

\langle n_1,\ldots,n_k\rangle = 2^{n_1}3^{n_2}\cdots p_k^{n_k}.

数项ff0的符号码序列是(3,3,1)，所以：

\ulcorner ff0\urcorner =2^3\cdot3^3\cdot5^1 =1080.

ff0在形式世界表示数2，而1080是符号串ff0的哥德尔数；三者不能混同。

算术基本定理保证素因数分解唯一，因此编码可逆。对序列再编码，便得到公式序列乃至形式证明的编码。形式系统的语法对象从此都变成自然数。

Godel Number Encoding：数项ff0、其符号序列和自然数1080属于三个不同层级。

10.7 秋天：原始递归性

10.7.1 原始递归函数

从常量、后继和投影函数出发，并对复合与下面的递归模式封闭：

F(0,\vec x)=G(\vec x),

F(n+1,\vec x) =H(n,\vec x,F(n,\vec x)).

例如阶乘：

\operatorname{factorial}(0)=1,

\operatorname{factorial}(n+1) =(n+1)\operatorname{factorial}(n).

计算输入n时，展开次数由n预先界定。具有原始递归特征函数的谓词称为原始递归谓词。

10.7.2 原始递归函数与谓词的性质

这类函数和谓词对以下操作封闭：

向原始递归函数代入原始递归函数；
对谓词取否定、合取、析取；
比较两个原始递归函数是否相等；
使用有界全称量词与有界存在量词；
在给定上界内搜索最小满足者。

加法、乘法、幂、相等与大小比较都属于这一范围。关键不是“函数写得短”，而是每个搜索和循环都有由输入给出的有限上界。

10.7.3 表现定理

是桥梁。对双变量原始递归谓词R(m,n)，存在形式系统P中的公式r(x,y)，使每个具体自然数m,n都满足：

R(m,n) \Longrightarrow P\vdash r(\overline m,\overline n),

\neg R(m,n) \Longrightarrow P\vdash\neg r(\overline m,\overline n).

谓词与命题属于含义世界；公式与无自由变量的语句属于形式世界。表现不是“公式大概描述了谓词”，而是每个具体输入的真假都能由相应语句或其否定的形式证明反映。

Representability Bridge：桥梁不是相似，而是对每个具体输入都能在P中反映真假。

10.8 冬天：通往可证明性的漫长之旅

10.8.1 整理行装

冬天要证明“p是x的形式证明”本身是原始递归谓词。原章连续定义46个函数与谓词，目的不是炫技，而是把证明检查器拆成每一步都有界的部件。

10.8.2 数论

定义1到5准备数论工具：

编号	名称	作用
1	`CanDivide(x,d)`	`d`能整除`x`
2	`IsPrime(x)`	`x`是质数
3	`prime(n,x)`	`x`按升序的第`n`个质因数
4	`factorial(n)`	阶乘
5	`p_n`	第`n`个质数

例如：

2352=2^4\cdot3\cdot7^2

对应质因数依次为2、3、7。所有搜索都附有可计算上界，因此保持原始递归。

10.8.3 序列

定义6到10把哥德尔数当作有限序列操作：

编号	名称	作用
6	`x[n]`	读取第`n`个质数的指数，即序列第`n`项
7	`len(x)`	求编码序列长度
8	`concat(x,y)`	连接两个序列
9	`singleton(x)`	构造只含`x`的序列
10	`paren(x)`	在编码序列外加左右括号

这就是解码器与序列库。

10.8.4 变量、符号、逻辑公式

定义11到33建立语法分析器和安全代换器：

编号	名称	作用
11-12	`IsVarType`、`IsVar`	判断变量类型与变量
13-15	`not`、`or`、`forall`	构造否定、析取、全称公式的编码
16-19	`succ`、`numeral`、`IsNumberType`、`IsNthType`	构造数项并检查类型
20-23	`IsElementForm`、`IsOp`、`IsFormSeq`、`IsForm`	从基本公式的生成序列判断合式公式
24-26	`IsBoundAt`、`IsFreeAt`、`IsFree`	判断变量位置受约束还是自由
27-31	`substAtWith`、`freepos`、`freenum`、`substSome`、`subst`	从后向前定位自由出现并完成无捕获代换
32	`implies`、`and`、`equiv`、`exists`	构造省略运算
33	`typelift`	只提升变量类型，不改变常量

IsFormSeq要求每个新公式由此前公式按语法构造，索引满足：

p,q\lt n.

这和形式证明相似，但此处检查的是“如何生成合式公式”，不是“如何由公理推出定理”。

10.8.5 公理、定理、形式证明

定义34到46把语法检查器升级为证明检查器：

编号	名称	作用
34	`IsAxiomI`	判断皮亚诺公理
35-36	`IsSchemaII`、`IsAxiomII`	判断命题逻辑公理模式
37-39	`IsNotBoundIn`、`IsSchemaIII(1)`、`IsSchemaIII(2)`	检查谓词公理及代换约束
40-42	`IsAxiomIV`、`IsAxiomV`、`IsAxiom`	判断集合公理并汇总全部公理
43	`IsConseq`	判断是否由两条推理规则直接推出
44	`IsProof`	每行是公理或此前行的直接推论
45	`Proves(p,x)`	`p`是形式证明且末行是`x`
46	`IsProvable(x)`	存在某个`p`满足`Proves(p,x)`

定义1到45只检查有限编码中的位置或有界候选，因此都是原始递归的。定义46：

\operatorname{IsProvable}(x) \quad\Longleftrightarrow\quad \exists p\,\operatorname{Proves}(p,x)

中的p没有预设上界。验证一份给定证明是机械可判定的；搜索是否存在任意长度证明则不再由原始递归性保证。

10.9 新春：不可判定语句

10.9.1 季节的确认

春天定义P，夏天给语法编码，秋天用表现定理把原始递归谓词送入P，冬天得到原始递归证明关系Proves(p,x)。新春再依次经过种子、绿芽、枝杈、叶子、蓓蕾、梅花、桃花、樱花。

10.9.2 种子：从含义世界到形式世界

设：

\operatorname{Diag}(y) = \operatorname{subst}(y,v,\overline y),

即把单变量公式编码y自身的数项代入其自由变量，得到对角化语句的编码。

定义原始递归谓词：

Q(x,y) \quad\Longleftrightarrow\quad \neg\operatorname{Proves}(x,\operatorname{Diag}(y)).

它说“x不是y对角化结果的形式证明”；去掉记号后，Q的含义就是“x不是y对角化结果的证明”。由表现定理，存在双变量公式q(x,y)在P中表示Q。原章把真、假两条表现路径记为B1和A1，后面分别沿蓓蕾与叶子继续。

10.9.3 绿芽：p的定义

把证明候选变量全称量化：

p(y):=\forall x\,q(x,y).

p(y)表达“没有任何x是y对角化结果的证明”。它只剩自由变量y。

10.9.4 枝杈：r的定义

原章再用单变量公式r整理q的特定实例与代换编码，让后续推导能在同一个哥德尔数层级上连接。关键不是新语义，而是保证每次“公式代入公式自身编码”的操作仍由先前定义的subst准确完成。

10.9.5 叶子：从A1往下走

把p的哥德尔数代入A1，再依次使用绿芽C2与枝杈C3、C4，得到A5：如果某个数确实编码了目标语句的证明，就能在P内推出与目标固定点相反的可证性结论。

10.9.6 蓓蕾：从B1往下走

同样把p代入B1，经C2、C3、C4得到B5：若某个数不是目标语句的证明，P能证明相应的r实例。A5与B5是梅花、桃花两次反证法的接口。

10.9.7 不可判定语句的定义

对p做自身代入：

g:=p(\ulcorner p\urcorner).

由构造可在P内得到固定点关系：

P\vdash g\leftrightarrow \neg\operatorname{Prov}_P(\ulcorner g\urcorner).

这不是把自然语言句子直接塞入系统，而是先给公式编码，再把编码的数项代回公式。目标是证明：

P\nvdash g, \qquad P\nvdash\neg g.

Fixed-Point Route：自我指涉通过数项和编码实现，最后分开检查g与否定g。

10.9.8 梅花：证明g不可证

假设P相容。再反设：

P\vdash g.

实际存在某个自然数s编码这条证明，所以证明关系的可表示性给出：

P\vdash\operatorname{Prov}_P(\ulcorner g\urcorner).

而固定点关系和P⊢g又给出：

P\vdash\neg\operatorname{Prov}_P(\ulcorner g\urcorner).

系统同时证明一式及其否定，与相容性矛盾。因此：

P\nvdash g.

原章特别区分两种矛盾：系统内部同时可证某公式及其否定，是形式世界的矛盾；“P相容”与推导出“P矛盾”冲突，是元数学命题层面的矛盾。

10.9.9 桃花：证明否定g不可证

原论文版本在这里假设。梅花已说明没有数真正编码g的证明，于是对每个具体候选t，P都能证明“t不是g的证明”这一实例。

若反设：

P\vdash\neg g,

由于¬g表达“存在g的证明候选”，便会与所有具体候选均被排除共同形成ω矛盾。因此在原章采用的条件下：

P\nvdash\neg g.

罗赛尔后来重构语句，使这一半也只需普通相容性。

10.9.10 樱花：证明P不完备

梅花与桃花合并：

P\nvdash g \quad\land\quad P\nvdash\neg g.

存在一个语句及其否定都不可证，所以P不完备。这是原章第一不完备定理证明旅行的终点。

10.10 不完备定理的意义

10.10.1 “我”是无法证明的

从元数学角度，g表达“g在P中没有形式证明”。它不同于骗子悖论：

“我是假的”若为真就为假，会直接造成语义悖论；
“我不可证”在相容系统中可以为真，同时不成为系统内定理。

由“数项化加哥德尔数化”实现，这正是。P的类型规则原本阻止同型对象直接作用于自己；编码把公式先送到自然数，再以数项代回，绕过的是表达路径，不是破坏语法规则。

原章用四句话概括建设性视角：

不完备性是发现之根；
相容性是存在之基；
同构映射是含义之源；
自我指涉是多产之泉。

10.10.2 第二不完备定理的证明之概要

令c是准确表达Con(P)的算术语句。第一定理的梅花证明可以在P内形式化为：

P\vdash \operatorname{Con}(P)\to g.

若反设P⊢c，由假言推理得到P⊢g；但只要P相容，梅花已经证明P\nvdash g。因此：

P\nvdash c.

也就是相容的P不能证明自身相容。把元数学证明内部化需要满足可证明性条件，原章明确把这一节称为“证明之概要”，没有把技术细节假装成一步。

10.10.3 不完备定理衍生的产物

第二定理能比较系统的相对强度。若系统Y能证明Con(X)，而X受第二定理约束，那么Y不可能与X拥有完全相同的证明能力；否则X也会证明自身相容。

追加公理不一定增加定理，因为新公理可能原本就是定理；但若扩张系统能证明原系统相容，就得到二者不等强的实质证据。“无法自证”在这里成为测量系统关系的工具。

10.10.4 数学的界限？

不完备定理不会让旧定理失效，也不等于数学“漏洞百出”。讨论必须先区分：

有明确符号、定义和规则的数学形式系统；
没有形式定义、只在思想中被称作“数学本身”的数学观。

前者可以成为不完备定理对象，后者属于数学论或哲学讨论。可以从数学定理获得启示，但不能把启示回写成“已由数学证明”的哲学结论。

10.11 带上梦想

10.11.1 并非结束

夜晚离开图书馆时，一整天的课程结束，研究却没有结束。莱布尼茨“计算逻辑”的梦想、哥德尔用数研究形式系统的证明与后来计算机之间出现历史连线。河流流入海并非水旅行的终点，知识的路线也不会在一条定理处封闭。

10.11.2 属于我

回程电车上，四人仍互相出题。米尔嘉以：

1,1,2,3,\ldots

无声提问，“我”用5回答，呼应最初相遇时的斐波那契数列。

音乐、逻辑、英语、数学分别属于同伴；“我”最终选择：

学习，以及传授，属于我。

这不是把不完备定理写成人生格言，而是整套叙事的学习结论：严谨区分对象和层级，同时把已经理解的东西传给身旁、远方与未来的人。

本章回顾：从形式化梦想走到可证明性边界

希尔伯特计划要求形式化、相容性证明和完备性证明。
相容表示不能同时证明A与¬A，完备表示二者至少一方可证。
矛盾系统可证明一切，因此按技术定义也是完备的。
第一不完备定理为满足条件的系统构造出系统内不可判定语句。
第二不完备定理限制系统证明自身相容性的能力。
定理讨论形式系统，不直接证明“数学有矛盾”或“理性有界限”。
形式系统P由七个常量、多型变量、递归公式语法、公理族与推理规则组成。
形式证明是每行都有机械许可证的有限公式序列。
哥德尔数用唯一质因数分解可逆编码符号、公式和证明。
原始递归性保证相关函数与有界检查可机械计算。
表现定理把原始递归谓词映成P中的公式。
定义1到45逐层构成Proves(p,x)，即给定证明候选的检查器。
IsProvable(x)使用无界存在量词，不等同于验证一份给定证明。
对角化把公式自身编码的数项代入其自由变量，构造固定点g。
在相容性条件下，若g可证就会让系统同时证明可证与不可证。
原章在ω相容条件下进一步证明¬g不可证。
g与¬g都不可证，所以系统不完备。
自指语句“我不可证”不是骗子语句“我是假的”。
第一证明可内部化为Con(P)→g，导出第二不完备定理。
第二定理可用于比较不同形式系统的相对强度。
数学定理与由其引出的数学观、哲学启示必须分层讨论。
原章最终把严谨研究与“学习、传授”的人物选择重新连接。

概念核对：五季路线的可验证节点

这份核对表把长证明拆成可检查的概念证据；每一项都要能在正文、图示、实验或练习中找到对应的层级与动作。

哥德尔不完备定理不是一句“存在不可证明真理”的口号，而是对满足条件的形式系统给出不可判定语句的精确结论。
希尔伯特计划把基础问题拆成形式化、证明相容性和证明完备性三项，后两项必须分别定义相容与完备。
相容条件要求A与¬A不能同时可证，完备条件要求A或¬A至少一方可证，两者组合才表达判定能力。
形式证明是有限序列，每一行要么是公理，要么由此前行按推理规则得到，末行才是待证定理。
形式系统的七个常量是0,f,¬,∨,∀,(,)；变量、类型、公式和规则在其上递归生成，而不是任意字符串都算公式。
类型层级让第n型变量表示低一型对象的集合，防止同型对象直接施加自我成员关系。
合式公式的逻辑公式递归生成只允许有限步骤；蕴含、合取、等价、存在量词都只是可展开的省略。
公理I到V分别覆盖公理I皮亚诺算术、命题逻辑、谓词逻辑、集合内涵和集合外延，公理族的分工不能混为一谈。
subst安全代换必须保持类型并避免变量捕获，否则把自由变量代入量词范围会改变公式含义。
元数学研究公式、证明和可证明性这些形式系统外的对象；它不是把人生格言换成数学符号。
哥德尔数让基本符号、公式序列和形式证明拥有自然数编码，从而可以被数论函数计算。
常量编码1 3 5 7 9 11 13使用不大于13的奇数，变量编码再用质数幂记录类型。
第n型变量编码为质数n次幂，因此从指数和质因数可以恢复变量的基名与类型层级。
序列的哥德尔数 2^{n1}3^{n2}…pk^{nk}把有限序列压成一个自然数，指数就是序列项。
ff0的编码是ff0的哥德尔数1080，但符号串、表示数2和自然数1080属于不同层级。
唯一质因数分解保证编码可逆；没有唯一性，就不能从一个自然数可靠地恢复原来的符号序列。
形式系统的一切可表示为数不是说数值和公式相同，而是说语法对象可以被数项间接指代。
原始递归函数从常量、后继和投影函数出发，通过复合与原始递归构造，所有递归展开都有输入给出的上界。
重复次数有上限是原始递归性的关键；它保证计算会在预先界定的有限步骤内完成。
复合与原始递归封闭，让加法、乘法、幂、阶乘和大小比较都落入同一套可计算构造。
原始递归谓词用特征函数表达真假，并可在否定、合取、析取和有界量词下继续构造。
有界全称量词与有界最小化都把搜索限制在输入给出的范围内，因此仍能机械计算。
表现定理是含义世界通往形式世界的桥梁，对每个具体输入把谓词真假对应到公式或其否定的可证明性。
谓词与命题属于含义世界，逻辑公式与语句属于形式世界；表现定理正是两种语言之间的受控翻译。
冬季定义的CanDivide、IsPrime、prime(n,x)和factorial(n)把数论工具拆成可复查的有限函数。
x[n]、len(x)、concat、singleton和paren构成序列解码器，让编码数可以再次作为公式构造的材料。
IsForm与subst分别检查递归语法和无捕获代换；验证证明与搜索证明不同，两者的量词范围不同。
IsAxiom汇总公理族，IsConseq检查推理规则，IsProof检查每一行，Proves(p,x)检查末行是否为x。
IsProvable(x) 使用无界存在量词寻找某个证明编码p，所以不能把它和验证一份给定证明的算法混同。
定义1到45只检查有限编码，定义46的无界存在量词没有预设上界，这正是证明搜索与证明验证的分界。
**Diag(y)**把公式编码y的自身数项代入自由变量，建立从语法对象到自身谈论的第一步。
**Q(x,y)**表达“x不是y对角化结果的证明”，表现定理把这一元数学谓词表示为系统P中的公式。
**p(y)=forall x q(x,y)**把证明候选全称量化，表达没有任何x是y自身代入结果的证明。
**g=p(⌜p⌝)**完成对角化固定点；它不是自然语言引号，而是编码和安全代换的形式构造。
g表达g不可证明是固定点关系的含义，但证明仍要在系统P的公式层级中逐步完成。
形式世界与含义世界的两种矛盾必须分开：一式及其否定同时可证是系统内矛盾，元数学假设冲突是另一层。
ω矛盾在原论文路线中排除“每个具体候选都不是证明、却整体证明存在证明”的组合，比普通相容性更强。
骗子悖论的“我是假的”直接制造语义循环；不完备性的自我指涉通过自然数编码绕开类型障碍。
数项化加哥德尔数化实现对象的间接自指，既不破坏语法规则，也不把含义世界的句子直接塞入形式系统。
第一证明的条件是相容性，第二半在原章版本使用ω相容性；这解释了为什么不能把两半证明写成同一个前提。
Con(P)推出g是第二定理概要的内部化关键；若P能证明Con(P)，便可在P内推出g并违背相容性路线。
P不能证明Con(P) 不表示P有矛盾，只表示相容系统不能在自身内部完成这条相容性证明。
形式系统相对强度可由Y证明Con(X)来比较；能证明更弱系统相容的系统拥有不同的证明能力证据。
最后一组1,1,2,3,5和“学习以及传授属于我”把严格的形式化工作重新接回叙事，而不是替定理添加哲学结论。

互动实验与四步复盘

先预测：如果只给出一条不可证明语句的结论，哪一步会被遗漏？切换四个阶段，观察“符号可检”“编码可算”“谓词可表示”“固定点可构造”如何闭合证明路线。

Incompleteness Route Lab

切换证明路线，保持层级不混