1.8 KiB
1.8 KiB
title, created, updated, type, tags, sources
| title | created | updated | type | tags | sources |
|---|---|---|---|---|---|
| 哥德尔编码 (Gödel Numbering) | 2025-04-15 | 2026-05-01 | concept |
哥德尔编码 (Gödel Numbering)
- 领域: 数理逻辑
- 发明者: 库尔特·哥德尔, 1931
- 来源: godel-incompleteness-tutorial
定义
哥德尔编码是将formal-systems中的符号、公式和证明序列唯一地映射为自然数的技术。通过质因数分解的唯一性，实现从元数学陈述到算术陈述的翻译。
编码规则
基本符号编码：为形式系统的每个基本符号分配一个唯一的自然数（如：0→1, S→2, +→3, ·→4, =→5, ¬→6, ∧→7, ∀→8, ∃→9, (→10, )→11, x→13, y→17, z→19...）
公式编码：若公式由符号序列 a₁a₂...aₖ 组成，各符号编码为 nᵢ，则：
GN(φ) = 2^{n_1} \cdot 3^{n_2} \cdot 5^{n_3} \cdot ... \cdot p_k^{n_k}
其中 pₖ 是第 k 个质数。
证明编码：若证明是公式序列 φ₁,...,φₖ，各公式编码为 gᵢ，则：
GN_{seq}(φ_1,...,φ_k) = 2^{g_1} \cdot 3^{g_2} \cdot ... \cdot p_k^{g_k}
算术化元数学
编码使得元数学概念转化为自然数的算术性质：
- 「x 是一个公式」→ 自然数 x 具有某性质
- 「x 是 y 的证明」→ 自然数 x 与 y 满足某关系
- 「公式 φ 可证」→ ∃x (x 是 GN(φ) 的证明)
这些算术性质在 peano-arithmetic 中可表达，这是哥德尔证明的核心创新。
关键应用
- 构造可表示的关系 Proof(x, y) 和 Prov(y)
- 定义替换函数 Sub(a, b, c)，实现self-reference
- 构造godel-incompleteness-theorems G = ¬Prov(Sub(n, n, n))
相关概念
diagonalization-method · self-reference · primitive-recursive-functions · metamathematics