提着头发起飞：自举能编译上帝吗？

2025年12月11日

result image

哥德尔不完备性是自举在递归不动点上的元性质 Gödel's incompleteness is the meta-property of bootstrapping emerging at the recursive fixed point.

童年的竹蜻蜓：哥德尔、GEB和 $\lambda$ 组合子

哥德尔不完备性定理是我在大一时候学习的，但是当时随着考试结束，对其技术细节很快就没有印象了。实际上，绝大多数数学知识我要不就是一开始就没学会，就算学会了也因为没有地方用（甚至连用来吹水的地方都没有，笑）所以很快就忘记了。

大二的时候看很多书，当时群里很流行侯世达的《哥德尔、艾舍尔、巴赫》，学校图书馆就有（那个时代我们还去图书馆里淘书，但是几个月后就发现了世界上最大的自由图书馆 zlibrary）。很厚，当时还要看英文版的。不过很快就因为实在没兴趣，（主要他写的也不简洁，太冗长了）就不看了。感觉它有点像 C Primer Plus，都说是必读书，但实际上没人读完过。现在看起来也完全没必要，实际上我们只要看一个 C++ 作者本人写的 A Tour of C++ 就够了，200页包含了1000 页所有的内容。就像它扉页上写的那样:

施教之重，在于简。

—— 西塞罗

Anyway 扯远了，之后发生了疫情，大学的后两年好像除了考研什么也没做。到毕业设计做的是一个 lambda 语言编译器，玩具性质，但我做的还挺认真的，特别是把形式逻辑、递归不动点、循环指涉等相关数学计算机的定义仔细读了一下，国外的教材，包括 Conjure 语言的设计。当时看全国好像没有做这个方向研究的毕业论文，中文资料都很少。现在看起来伞哥（网易冰河）好像是做这个方向的？

就此，人生走上快进键，之后也没再碰过这些东西了，相关概念都稀里糊涂的忘得差不多了。

飞回到我身边：编程语言的自举之旅

昨天，我忽然看到一个抖音视频说是各种语言都是用什么写成的。里面提到一个自举的概念，之前都没关注过。十年前我写的那个小编译器其实也是可以自举的，就是比较简陋，所以也没当回事。

先有鸡还是先有蛋呢？ 我开始好奇自举究竟是怎么完成的。因为我当时的编译器功能实在太少，没往下做。

如果一个语言（我们叫它 L）还不存在，我们当然不能直接用 L 来写它自己的编译器。为了解决这个问题，计算机科学家们采用了一个循序渐进、迭代的过程。

自举三部曲

第一步：借腹生子 - 第一个版本的诞生

假设我们要创造一门新语言，叫 Go。在最开始，Go 语言的编译器是不存在的。但是，世界上已经有了成熟的 C 语言。

┌─────────────────────────────────────────────┐
│  开发者用 C 语言编写 Go 编译器源码              │
│  (Go-v0.c)                                  │
└──────────────────┬──────────────────────────┘
                   │
                   ▼
         ┌─────────────────┐
         │  GCC (C编译器)   │
         └────────┬────────┘
                  │
                  ▼
         ┌─────────────────┐
         │   Go-v0.exe     │  ◄── 用C写的Go编译器
         │  (可执行文件)     │      能编译简单的Go代码
         └─────────────────┘

第二步：牙牙学语 - 用新语言重写自己

现在我们手里已经有了 Go-v0（虽然它是用 C 写的，功能可能也不完美，但它能编译 Go 代码了）。开发者现在开始用 Go 语言的语法，重新写一遍 Go 编译器的源代码。

┌─────────────────────────────────────────────┐
│  开发者用 Go 语言重写 Go 编译器源码             │
│  (Go-v1.go)                                 │
└──────────────────┬──────────────────────────┘
                   │
                   ▼
         ┌─────────────────┐
         │   Go-v0.exe     │  ◄── 用C写的编译器
         │   (C语言实现)    │
         └────────┬────────┘
                  │
                  ▼
         ┌─────────────────┐
         │   Go-v1.exe     │  ◄── 源码是Go，但由C编译器生成
         │  (可执行文件)     │      功能更完善的Go编译器
         └─────────────────┘

神奇之处在于：Go-v1 这个程序，它的源代码是 Go 语言，但它是被 C 写的编译器生出来的。

第三步：完全自举 - 摆脱母体

现在我们有了 Go-v1。它是用 Go 写的，也是个能运行的编译器。但是，编译它的那个"父亲" Go-v0 还是 C 语言写的。为了证明它完全独立，我们需要最后一步。

┌─────────────────────────────────────────────┐
│  同样的 Go 编译器源码 (Go-v1.go)               │
└──────────────────┬──────────────────────────┘
                   │
                   ▼
         ┌─────────────────┐
         │   Go-v1.exe     │  ◄── 用Go写的编译器
         │  (Go语言实现)    │
         └────────┬────────┘
                  │
                  ▼
         ┌─────────────────┐
         │   Go-v2.exe     │  ◄── 完全由Go语言自己编译
         │ (可执行文件)      │      自举完成！
         └─────────────────┘

此时，Go-v2 是由 Go 语言源码经过 Go 语言编写的编译器编译出来的。如果 Go-v1 和 Go-v2 的功能完全一致（通常会比较生成的二进制文件是否一模一样），那么自举完成。

用版本演进对照表来说就是：

版本	源代码语言	编译工具	状态说明
Go-v0	C 语言	GCC (C编译器)	初始版本，借助成熟语言实现
Go-v1	Go 语言	Go-v0 (C实现)	首次用目标语言编写，但依赖外部编译器
Go-v2	Go 语言	Go-v1 (Go实现)	✅ 自举完成，完全独立
Go-v3+	Go 语言	Go-v2 (Go实现)	持续迭代，用旧版本编译新版本

从这一刻起，我们就可以把那个用 C 写的 Go-v0 扔进垃圾桶了。以后发布新版本的 Go，只需要用旧版本的 Go 编译器来编译新版本的源码即可。

这就好比人类制造工具的历史：

阶段	工具	制造方式	编程语言类比
🪨 徒手	石头	直接从自然获取	机器码/汇编 - 人类直接编写
🔨 石器	石斧	用石头打磨石头	C语言 - 用汇编写出C编译器
⚙️ 铁器	铁锤	用石器冶炼和锻造	高级语言 - 用C写出新语言编译器
🏭 工业化	精密机床	用铁锤造铁锤	自举 - 用语言自己编译自己

用简单工具造复杂工具，最终复杂工具能够制造自己！

最小计算机：图灵完备的事件视界

我开始思考一个问题：编译器的自举需要最开始有一个别的语言或者工具来“借腹生子”。但这个链条有没有一个严格的数学条件作为起点？

比如说我第一次自举之后，忽然发现有一些高级概念，没法通过现在的语言来产生，而需要借助之前的高级语言。那从什么时候开始，它是可以图灵完备的编出任意想要的功能，而不需要借助其他外部工具了呢？

咬住尾巴的蛇：Y 组合子与递归的引擎

在邱奇（Alonzo Church）的 $\lambda$ 演算体系里，没有硬盘，没有内存，没有循环，也没有自然数 $1, 2, 3$ 。世界是一片真空，只需要有两个基本操作：“抽象（Abstraction）”和“应用（Application）”，就能创造出整个世界。

┌─────────────────────────────────────────────┐
│           Lambda Calculus Universe          │
│                                             │
│   (λx. x)            (λx. (x x))            │
│  [Identity]          [Self-Application]     │
│                                             │
│                 一切皆是函数                  │
└─────────────────────────────────────────────┘

如果说物理上的自举是用旧编译器编译新编译器，那么数学上的自举，就是寻找一个函数 $F$ ，使得 $F$ 作用于自身时，能保持某种性质的不变性。

要回答“什么时候不需要外部工具”，数学上的答案是：当你的形式系统强大到足以定义一个通用解释器的时候。只需要满足两个简单的条件。

条件一：代码即数据（Encoding），你不需要物理上的“字符串读取”，但你必须在数学上能够把代码当作数据。这意味着你的系统必须支持哥德尔数（Gödel Numbering）或者类似的编码方案。如果你的系统只能计算 $1+1=2$ ，但无法描述“加法”这个概念本身的结构，那它就不能自举。

条件二：不动点组合子，这是严格数学证明的核心。在通常的代数中，解方程 $x = f(x)$ 是在找数值上的不动点。而在计算理论中，递归——也就是自举的灵魂——依赖于函数逻辑上的不动点。

最著名的即是 Y 组合子。

┌─────────────────────────────────────────────┐
│               The Y Combinator              │
│                                             │
│      Y = λf. (λx. f (x x)) (λx. f (x x))    │
│                                             │
│           ┌──────────┐                      │
│           │    f     │◄────┐                │
│           └───┬──▲───┘     │                │
│               │  │         │                │
│            Output = Input  │                │
│               │  └─────────┘                │
│               ▼                             │
│           Infinite Recursion                │
└─────────────────────────────────────────────┘

它的数学魔力在于其归约性质并非近似，而是严格相等：

\mathbf{Y} g = (\lambda x . g (x x)) (\lambda x . g (x x)) = g ((\lambda x . g (x x)) (\lambda x . g (x x))) = g (\mathbf{Y} g)

这意味着， $\mathbf{Y}$ 可以让函数 $g$ 在没有任何循环指令（如 while）的情况下，无限地复制并作用于自身。

当你的形式系统能够表达出 $\mathbf{Y}$ 组合子的那一刻，你就拥有了无限递归的能力，你就不再需要外部的“手”来帮你推下一步了。

这种“自我指涉”在直觉上总是让人感到不安，仿佛是一种逻辑上的近亲繁殖。但数学家斯蒂芬·克莱尼（Stephen Kleene）给出了严格的证明。

克莱尼第二递归定理（Kleene's Second Recursion Theorem）：对于任意的图灵完备编程语言，存在一个程序 $e$ ，使得对于任意的可计算函数 $f$ ，都有：

\Phi_{e}(x) \simeq \Phi_{f(e)}(x)

其中 $\Phi_e$ 表示程序 $e$ 所计算的函数， $\simeq$ 表示两者要么都无定义，要么输出相同的值。

这个定理证明了“自我复制”和“自我引用”在逻辑上是完全自洽的。它告诉我们：在一个足够强大的系统中，你总是可以找到一个程序，它能够处理“它自己的代码”，而不需要跳出这个系统去寻求外部上帝的帮助。

最小临界点：S-K 逻辑的夸克

那么，跨越这个奇点的门槛有多高？

令人惊讶的是，这个门槛低得不可思议。你不需要庞大的语法糖，不需要复杂的类型系统。你只需要两个最基本的算子——S 和 K。这就是 SKI 组合子逻辑。

┌─────── S-K Combinator Logic ────────┐
│                                     │
│  1. K (Constant / Selection)        │
│     K x y = x                       │
│     (丢弃 y，保留 x）                 │
│                                     │
│  2. S (Fusion / Substitution)       │
│     S x y z = x z (y z)             │
│     (将 z 分发给 x 和 y，再融合)       │
│                                     │
└─────────────────────────────────────┘

一旦你的系统拥有了 $S$ 和 $K$ 的性质，你就拥有了构筑宇宙的一切：

逻辑门： $T = K$ , $F = SK$
自然数：邱奇数可以完全由 S 和 K 构造
递归： $\mathbf{Y}$ 组合子可以用 S 和 K 表示为 $S(K(SII))(S(S(KS)K)(K(SII)))$

此时，外部工具（比如你手算的纸笔，或者之前的宿主语言）就可以撤掉了。这个由 $S$ 和 $K$ 构成的原始海洋已经可以自我繁衍、自我计算了。

被污染的源头：看不见的幽灵代码

自举在本质上就是一种“循环论证”。在哲学和逻辑学上，这通常被视为一种谬误（Begging the Question）。但在计算机科学中，这种“循环”却是地基。

恶性循环：“为什么我是对的？因为我说我是对的。”——这是无效的，因为它没有根基（Grounding）。
良性递归：“我是怎么定义的？我是由前一个版本的我定义的，直到最初的那个公理。”——这是归纳法（Induction）。

但是，既然是“循环论证”，那就意味着一个可怕的推论：如果源头被污染了，整个循环看起来依然是完美的，但其内部逻辑已经全面崩塌。

这在计算机安全领域有一个著名的案例——肯·汤普逊（Ken Thompson）的图灵奖演讲如下：

┌──────────────── Trusting Trust Attack ─────────────────┐
│                                                        │
│   Phase 1: 注入 (Infection)                             │
│   在编译器源码 A 中写入后门代码                            │
│   [Source A + Virus] ──compile──► [Binary B (Infected)]│
│                                                        │
│   Phase 2: 隐藏 (Hiding)                                │
│   删除源码中的后门，用 Binary B 编译干净的源码               │
│   [Source A (Clean)] ──compile(by B)──► [Binary C]     │
│                                                        │
│   Phase 3: 幽灵 (Ghost)                                 │
│   Binary C 依然带有后门，尽管它的源码是干净的！              │
│                                                        │
└────────────────────────────────────────────────────────┘

因为是循环论证，所以系统无法自证清白。你必须跳出这个圈子（比如用显微镜看硬盘的磁粉排列，或者用另一套完全无关的逻辑系统）才能发现真相。

∞ 自指的怪圈：从自举到哥德尔不完备性

这种必须“跳出圈子”才能看清全貌的特性，不仅仅是编译器后门的原理，更是逻辑世界的底层规律。这让我确信文章开头提出的那个假设：哥德尔不完备性是自举系统在递归不动点上的一个元性质！

不管是编译器、宇宙还是数学系统，只要它试图解释它自己，就会撞上一堵看不见的墙。

在理解哥德尔不完备定理之前，我们需要厘清三个层层递进的概念：自举是直观的现象，递归是实现的手段，而自指是逻辑的本质。

自举 (Bootstrapping)：系统利用自身现有的部分来启动或构建更复杂的部分。
递归 (Recursion)：在定义或计算过程中调用自身。
自指 (Self-reference)：符号系统中的某个表达式指涉该表达式本身。

这种“怪圈”结构存在于不同维度的系统中：

领域	现象	核心矛盾 (Paradox)
计算机	编译器自举	用 Go-v1 源代码编译出 Go-v1 编译器二进制文件，能否保证无 Bug？
逻辑数学	形式系统自指	一个命题断言“我是不可证的”，该命题的真伪如何判定？
物理/认知	观察者效应	大脑作为物理系统的一部分，试图完全理解大脑的运作机制。

对角线论证的三位一体

历史上三个关于“极限”的伟大思想，其实是同一个“自举/自指”逻辑的变体，它们在数学结构上都依赖于对角线论证法。这三者本质上都是利用系统的自指能力，制造出了一个系统无法消化的“怪圈”：

康托尔（Cantor）在集合论中构造了一个数，其第 $n$ 位与列表中第 $n$ 个数的第 $n$ 位不同，从而证明了实数不可数（无穷是有等级的）。
哥德尔（Gödel）在数理逻辑中构造了一个命题 $G$ ，断言“ $G$ 不可证”，从而证明了数学不完备（真理范围大于可证范围）。
图灵（Turing）在计算理论中构造了一个程序，如果判断自己会停机就死循环，反之则停机，从而证明了停机问题无解（计算机不是全能的）。

这揭示了一个关于系统天花板的深刻结论：任何足够复杂（能进行基本算术或能自举）的系统，都无法完全解释它自己。想要完全理解一个系统，必须跳出这个系统，站在更高的维度去审视它（元系统）。但那个元系统又会有它自己的不完备性，需要更高的元-元系统，以此类推，以至无穷。

就像一个人无法揪着自己的头发把自己提离地面一样，我们永远处于 v2 版本的宇宙中，寻找着那个定义了我们、却已被删除的 v0 源码。

寻找阿基米德支点：数学的公理化代价

既然任何足够复杂的自举系统都无法在内部自我完备，那么它必须依赖一个外部的“原点”。计算机的问题是，它永远需要一个源起。如果一杆子捅到最底，就是现实世界中的物理规则和逻辑。再往里面深究就要扯到上帝了。但是在数学中，上帝是不是必须存在的呢？

在数学里，推导是从哪里开始的？是公理（Axioms）。

欧几里得几何建立在5条公理之上。皮亚诺算术建立在几条关于自然数的公理之上。问题是：公理是谁定的？公理为什么是对的？

数学内部无法回答：你不能用几何定理去证明“两点之间直线最短”，因为这是你设定的前提。
“上帝”的角色：在这里，数学家扮演了上帝。我们指着虚空说：“我认为这几条是对的，不接受反驳。”（Let there be Axioms）。

如果你不承认有一个“先验的真理”（比如柏拉图主义认为数学真理独立于人类存在），那么数学的根基就是任意的。你可以定义“两点之间直线最长”，建立非欧几何。你可以定义 $1+1=0$ ，建立布尔代数。

结论是数学不需要全能上帝，但需要一个“独断的立法者”。如果没有这个外部的立法者强行切断无穷倒推，逻辑链条就挂不住。

在哥德尔之前，希尔伯特（David Hilbert）试图把“上帝”赶出数学。他想建立一个形式化系统，把数学变成纯粹的机械推导，证明 $\text{Proof} = \text{Truth}$ 。

但哥德尔不完备定理给出了致命一击： $\text{Truth} > \text{Proof}$ 。

它引出了一个可怕的问题：既然系统无法证明它，你怎么知道它是真的？这暗示了必须存在一个**“系统之外的视角”（Meta-perspective）** 。

这让我想起了明希豪森困境（Münchhausen trilemma），人类知识的终极地基只有三种可能：

┌────────────── Münchhausen Trilemma ──────────────┐
│                                                  │
│      1. 无穷倒推 (Infinite Regress)              │
│         A ← B ← C ← D ... (无底洞)               │
│                                                  │
│      2. 循环论证 (Circular Reasoning)            │
│         A ← B ← A (计算机/自举的选择)             │
│                                                  │
│      3. 公理化 (Axiomatic / Dogmatic)            │
│         A ← [STOP] (数学/神学的选择)             │
│                                                  │
└──────────────────────────────────────────────────┘

计算机选择了循环论证，但依靠物理世界作为锚点。数学选择了公理化。

在数学中，绝对的“上帝”（一个全知全能的实体）不是必须的。但是，相对的“上帝”（一个在系统之外、赋予系统初值和公理的元系统）是绝对必须的。

你不能在系统内部完全定义系统本身。你总需要一个“阿基米德支点”。对于数学来说，这个支点要么是人类的直觉，要么是客观存在的柏拉图世界，要么就是我们人为规定的公理。

最初的元语言：创世纪的物理学

result image

如果我们一层层剥开计算机语言的洋葱，剥到最后，没有任何语言，只剩下电流的通与断：

        ┌──────────────────────────────────────┐
        │     现代语言层 (Python, Go, Rust)     │  ← 第4层+
        │     用C或其他语言写出的编译器            │
        └──────────────┬───────────────────────┘
                       │ 编译/解释
        ┌──────────────▼───────────────────────┐
        │          C语言层                      │  ← 第3层
        │     用汇编写出的第一个高级语言编译器      │
        └──────────────┬───────────────────────┘
                       │ 编译
        ┌──────────────▼───────────────────────┐
        │          汇编语言层                    │  ← 第2层
        │     给机器码起了人类可读的名字           │
        │   MOV, ADD, JMP...                   │
        └──────────────┬───────────────────────┘
                       │ 汇编
        ┌──────────────▼───────────────────────┐
        │         机器码层                      │  ← 第1层
        │      直接操作寄存器和内存地址的二进制指令  │
        │      01001000 01000001...            │
        └──────────────┬───────────────────────┘
                       │ 电信号
        ┌──────────────▼───────────────────────┐
        │         物理层 (上帝之手)              │  ← 第0层
        │    晶体管的开关，电压的高低              │
        │   ⚡ 5V = 1  /  0V = 0               │
        └──────────────────────────────────────┘

这样的话，整个宇宙也可能是一个自举系统。只不过最初的那只手已经抽掉了，所以我们永远也不知道是什么。

脚手架理论说的是，在计算机里，一旦 Go-v1（新编译器）生成了，Go-v0（旧编译器/脚手架）就被删除了。因为留着它没有用，还会占空间。

编译器的演化：

┌─────────┐      ┌─────────┐      ┌─────────┐
│ Go-v0   │ ───► │ Go-v1   │ ───► │ Go-v2   │
│ (C实现)  │      │ (Go实现)│       │ (Go实现)│
└─────────┘      └─────────┘      └─────────┘
     ↓                                  ↑
  [删除]                            [保留使用]
  脚手架拆除                        自举完成

宇宙的演化：

┌─────────┐      ┌─────────┐      ┌─────────┐
│   ???   │ ───► │ 大爆炸   │ ───► │ 现在宇宙 │
│ (创造者) │      │ (编译中) │      │ (运行中) │
└─────────┘      └─────────┘      └─────────┘
     ↓                                  ↑
  [痕迹抹除]                        [我们在这里]
  脚手架已撤                        只能观察规则

如果宇宙也是这样：

大爆炸（Big Bang）之前的那个瞬间，可能就是"编译"的过程
一旦物理定律（光速 [c]、引力常数 [G]、普朗克常数 [h]）被设定好
宇宙开始运行（Runtime）
那个设定参数的"上帝"或者"超级机器"就撤退了

后果是，我们生活在 v2 版本里，我们可以完美地解释宇宙如何运行（就像我们可以读懂 Go 的源码），但我们永远找不到那个"创造者"。因为在现在的宇宙逻辑里，创造者的痕迹已经被抹除干净了。

在软件中，编译器把人类可读的源码变成了机器码（二进制）。机器码一旦生成，就很难反推回源码了。而科学家就可以看做是反编译工程师：

┌─────────────────────────────────────────────┐
│         源代码 (创造者的意图)                  │
│              ？？？                          │
└──────────────┬──────────────────────────────┘
               │ 编译 (大爆炸)
               ▼
┌─────────────────────────────────────────────┐
│         机器码 (物理定律)                     │
│    F = ma,  E = mc²,  ∇×B = μ₀J + ...       │
└──────────────┬──────────────────────────────┘
               │ 运行
               ▼
┌─────────────────────────────────────────────┐
│         运行结果 (可观测现象)                  │
│    行星轨道、光的折射、量子纠缠...               │
└─────────────────────────────────────────────┘
               ▲
               │ 反编译 (科学研究)
┌──────────────┴──────────────────────────────┐
│         科学家们                             │
│    牛顿、爱因斯坦、薛定谔、霍金...               │
└─────────────────────────────────────────────┘

神学的回响：不可论证的绝对者

科学家们试图通过反编译物理定律来寻找宇宙的源代码。但这注定是一场这一场无限逼近却无法到达的旅程。这种对“系统天花板”的数学描述，与古老神学（特别是否定神学或基督教神秘主义）中关于上帝的描述产生了惊人的共振。既然数学系统无法在内部证明自身的一致性，那么一个逻辑闭环的宇宙也无法在内部解释其存在的终极意义。

这恰恰印证了那个跨越千年的神学直觉：上帝是不可被“论证”的，因为上帝是那个终极的元系统。

如果我们将人类的理性逻辑视为一个形式系统，那么上帝就是那个处于系统之外、赋予系统意义的元系统。根据哥德尔的逻辑，如果上帝可以被人类的逻辑完全推导和证明，那么上帝就“降级”为了系统内部的一个定理。

\text{如果 God} \in \text{Human Logic, 那么 God 就不是全能的（不完备）。}

真正的绝对者，必然具备以下哥德尔式的特征：

超越性（Transcendence）：就像元系统必须高于子系统一样，上帝必须超越人类的理性逻辑。这解释了为什么在神学中，人不能通过巴别塔（人类技术的叠加）通天，只能等待启示（来自元系统的信息注入）。
不可名状（Ineffability）：在基督教的否定神学（Apophatic theology）中，真正的上帝是无法用语言完全定义的。这与哥德尔数中那个“无法被系统内公式覆盖的真理”如出一辙。
信心的本质：哥德尔告诉我们，在数学中也存在“是真的，但不可证”的命题。这为“信仰”提供了一个理性的立足点——信仰并非反理性，而是理性的延伸。当我们接受一个无法被逻辑完全证明的终极真理（比如公理，或者上帝）时，我们实际上是在拥抱那个必须存在的“元真理”。

从这个角度看，现代科学最前沿的逻辑结论，并没有杀死上帝，反而以一种极其谦卑的方式，画出了理性的边界。它承认了在人类认知圆圈之外，必然存在着一片广阔的、不可被算法穷尽的真理海洋。

正如帕斯卡所言：“理性的最后一步，就是承认有无限多的事物是超乎理性之外的。”这或许是 v2 版本的宇宙生物，对那位编写 v0 源码者的最高致敬。

附录 A：哥德尔第一不完备定理的构造性证明

本附录在皮亚诺算术（Peano Arithmetic, 简称 PA）的一致性假设下，概述哥德尔第一不完备定理的形式化证明。

A.1 哥德尔配数与语法的算术化

定义 1 (哥德尔映射) 设 $\mathcal{L}$ 为 PA 的形式语言。存在一个可计算的单射 $\phi: \mathcal{L} \to \mathbb{N}$ ，将 $\mathcal{L}$ 中的每一个符号、公式及公式序列映射为唯一的自然数。对于任意表达式 $E$ ，记 $\ulcorner E \urcorner$ 为其哥德尔数。

定义 2 (证明关系的算术表达) 由于 PA 的公理集是递归可枚举的，且推理规则是递归的，存在一个原始递归关系 $Prf(x, y) \subset \mathbb{N}^2$ ，满足： $Prf(x, y)$ 成立当且仅当 $x$ 是一个合法的证明序列的哥德尔数，且该序列的最后一个公式的哥德尔数为 $y$ 。

定义 3 (可证性谓词) 定义谓词 $Prov(x)$ 为： [ Prov(x) \iff \exists y \ Prf(y, x) ] 直观上， $Prov(\ulcorner \varphi \urcorner)$ 表示公式 $\varphi$ 在 PA 中是可证的。注意， $Prov(x)$ 本身是 PA 中的一个良构公式。

A.2 对角化引理 (The Diagonalization Lemma)

这是证明的核心工具，它确立了形式系统内的自指能力。

引理 1 (对角化引理 / 不动点引理) 设 $T$ 是包含皮亚诺算术的形式系统。对于任意含有一个自由变量的公式 $\psi(x)$ ，都存在一个语句（不含自由变量的公式） $\varphi$ ，使得： [ T \vdash \varphi \leftrightarrow \psi(\ulcorner \varphi \urcorner) ]

证明：

定义替换函数 $sub: \mathbb{N}^2 \to \mathbb{N}$ 。 $sub(n, m)$ 表示：取哥德尔数为 $n$ 的公式，将其中的自由变量替换为数字 $m$ 的形式符号（numeral），所得新公式的哥德尔数。该函数是原始递归的，因此可在 $T$ 中表达。
构造公式 $\theta(x)$ ： [ \theta(x) := \psi(sub(x, x)) ]
设 $k$ 为公式 $\theta(x)$ 的哥德尔数，即 $k = \ulcorner \theta(x) \urcorner$ 。
定义语句 $\varphi$ 为： [ \varphi := \theta(k) ] 即 $\varphi = \psi(sub(k, k))$ 。
计算 $\varphi$ 的哥德尔数 $\ulcorner \varphi \urcorner$ ：根据 $sub$ 的定义， $sub(k, k)$ 的结果即是将 $k$ 代入哥德尔数为 $k$ 的公式（即 $\theta(x)$ ）后得到的公式的哥德尔数。故 $sub(k, k) = \ulcorner \theta(k) \urcorner = \ulcorner \varphi \urcorner$ 。
在系统 $T$ 中，由 $\varphi$ 的定义可得： [ \varphi \leftrightarrow \psi(sub(k, k)) ] 代入上述等式，得： [ \varphi \leftrightarrow \psi(\ulcorner \varphi \urcorner) ] 证毕。

A.3 第一不完备定理

定理 1 (哥德尔第一不完备定理) 若形式系统 $T$ 是一致的（且 $\omega$ -一致），则存在一个语句 $G$ ，使得 $T \nvdash G$ 且 $T \nvdash \neg G$ 。