哥德尔数

定义

在形式数论中，哥德尔数指某个形式语言里每个符号与合式公式所对应的唯一自然数，建立这种对应关系的函数称为哥德尔编号^[1]。中文工具书把它界定为对形式系统中的符号、公式和证明所指派的自然数，也称哥德尔配数、哥德尔码数^[2]。同一个表达式在不同编号方案下会得到不同的数，但同一方案内部是一一对应的^[5]。

被编码的对象不限于单个公式。符号串、公式的有限序列乃至一整段证明，都可以先各自取哥德尔数，再把这些数串起来重新编码，从而得到代表整段证明的单个自然数^[3]。哥德尔本人在两个层次上使用了这一方案，先编码公式序列，再编码证明序列^[5]。

原理

构造哥德尔数通常分两步。第一步给形式语言的每个初始符号固定一个自然数，称为该符号的符号数；如何排序是任意的，但一经选定便保持不变^[3]。第二步再把符号数组成的有限序列压缩成一个数，常用手段是以素数幂的乘积来编码^[3]。

设符号数序列为 $(n_0,n_1,\dots,n_k)$，$p_1,p_2,\dots$ 依次为素数，则该序列对应的哥德尔数为 $c=2^{n_0}\times 3^{n_1}\times 5^{n_2}\times\cdots\times p_{k+1}^{n_k}$^[3]。例如按某套符号编号，公式 $0=0$ 的符号数序列为 $(1,5,1)$，其哥德尔数是 $2^1\times 3^5\times 5^1=2430$^[3]。

这套编码可以逆向读取，依据是算术基本定理：任何大于 1 的自然数都能唯一地分解为素因数的乘积，因此对一个哥德尔数作素因数分解，就能还原指数序列并恢复最初的符号串^[3][5]。这种把逻辑表达式翻译成算术对象的技术也被称为算术化^[6]。

flowchart LR

A[符号串] --> B[查符号编号表]

B --> C[得到符号数序列]

C --> D[以素数为底求幂并相乘]

D --> E[哥德尔数]

E --> F[素因数分解]

F --> G[还原符号数序列]

发展历程

哥德尔在 1930 年 11 月 17 日提交、1931 年发表于德文期刊《数学与物理学月刊》的论文《论〈数学原理〉及其相关系统中的形式不可判定命题》中引入了这一方法^[7]。该论文的主要结论是哥德尔第一与第二不完备定理，分别对应文中的定理 VI 与定理 XI，而哥德尔编号正是证明它们的关键手段^[7]。

由于方法新颖，且为避免歧义，论文列出了 45 个原始递归函数与关系的明确定义，用于操作和检验哥德尔数，并据此定义了谓词 Bew，它在且仅在某个数是可证语句的哥德尔数时成立^[7]。论文发表时，递归函数的现代术语尚未确立，哥德尔用 rekursiv 一词指称今天所说的原始递归函数^[7]。

此后，类似的编码被用于计算模型。1936 年，图灵把图灵机的指令表编码成整数，即该机器的哥德尔数，写在通用图灵机的输入带上，使后者能够模拟任意一台机器。自 1931 年那篇论文之后，哥德尔编号、哥德尔码等说法也被用来泛指把自然数指派给各种数学对象的做法^[1]。

应用

哥德尔数最直接的用途是让形式系统谈论自身。把公式的哥德尔数代回公式，可以构造出内容为“本语句不可证”的自指语句，对角线引理把这一手法推广到任意公式，从而在系统内部表达关于可证性的命题^[4]。哥德尔正是借此证明，足够强的一致形式系统中存在既不可证也不可否证的命题^[8]。

在可计算性理论中，哥德尔型编码使程序可以当作数据来传递。给图灵机编号之后，“某台机器在某个输入上是否停机”这一问题可以化为自然数之间的算术问题，并最终被证明不可判定。通用图灵机读取目标机器的编号并模拟其行为，这一思路与现代计算机把程序存放在存储器中执行的做法相通。

在部分文献中，可计算函数集合的编号也被称为哥德尔编号或有效编号，哥德尔编号可被理解为一种编程语言，其中每个可计算函数的哥德尔数相当于在该语言里计算它的程序^[5]。

局限

哥德尔编号并不唯一。给基本符号安排不同的编号或不同顺序，同一组表达式就会得到另一套哥德尔数；只要把 K 个基本符号按固定次序映射到 K 进制数字，就能得到一种自洽的编号方案^[5]。选取哪一种方案并不影响定理的成立，只影响具体数值^[1]。

编码所得的数往往极其庞大，但这并不构成障碍，关键只在于这样的数能够被构造出来^[1]。方法还要求编码是有效的、纯机械的，即存在有限步骤的例行程序完成编解码，并且能够判定一个给定的数是否真的编码了某个表达式^[3][4]。

更根本的限制来自哥德尔数所服务的结论本身。对于包含初等数论的足够强且一致的形式系统，总存在系统内既不能证明也不能否证的命题，因此这套编码并不能让系统摆脱不完全性^[8]。类似地，给程序编号也不能使停机问题变得可以判定。

参见

• 哥德尔不完备定理 —— 借助哥德尔数把自指语句形式化后得到的基础性结果。

• 形式系统 —— 哥德尔数所编码的符号、公式与证明所在的演算体系。

• 图灵机 —— 可用哥德尔数编号并在通用机上加以模拟的计算模型。

• 停机问题 —— 通过给程序编号而证明其不可判定性的问题。

• 对角线论证 —— 构造自指语句时与哥德尔编码配合使用的证明方法。

• 算术基本定理 —— 保证素数幂编码可以唯一还原的定理。