哥德尔编码

哥德尔编码是一种将形式系统中的符号、公式和证明映射到自然数的方法，通过这种编码，形式系统的元数学命题（如“公式A可证明”）可转化为关于自然数的算术命题。以下是逐步讲解：

1. 基本思想

   • 目标：将形式语言中的对象（如逻辑符号、变量、公式序列）唯一地对应到自然数，使得这些对象的性质可通过自然数的算术性质来描述。
   • 核心工具：算术基本定理（自然数的质因数分解唯一性）。

2. 符号编码

   • 假设形式系统有有限个基本符号（如逻辑联结词¬、→，量词∀，括号，变量x₁, x₂, …）。
   • 为每个符号分配一个奇数编码（例如：¬→1, →→3, ∀→5, (→7, )→9, xₖ→2k+1）。
   • 变量编码需可扩展，因此变量xₖ的编码通常设计为与k成线性关系（如2k+1）。

3. 公式的编码

   • 一个公式是符号的序列（如∀x₁ (x₁ = x₁)）。
   • 设公式由n个符号组成，符号编码分别为c₁, c₂, …, cₙ。
   • 取前n个质数p₁=2, p₂=3, …, pₙ，计算：

\[ \text{Gödel number} = p_1^{c_1} \cdot p_2^{c_2} \cdots p_n^{c_n} \]

• 例如：若¬的编码为1，x₁的编码为3，则公式¬x₁对应质数幂乘积2¹·3³=54。

4. 证明序列的编码
   • 一个证明是公式序列（F₁, F₂, …, Fₘ），每个公式已有哥德尔数g₁, g₂, …, gₘ。
   • 对序列编码：取前m个质数q₁=2, q₂=3, …, qₘ，计算：

\[ \text{Gödel number of proof} = q_1^{g_1} \cdot q_2^{g_2} \cdots q_m^{g_m} \]

• 这样，证明的哥德尔数通过质因数分解可还原出每一步的公式。

5. 元数学的算术化

   • 通过编码，形式系统中的句法关系（如“公式A是公理”“序列P是公式B的证明”）可定义为自然数上的谓词。
   • 例如：谓词\(\text{Proof}(m, n)\)表示“m是哥德尔数为n的公式的证明的哥德尔数”。
   • 哥德尔在不完备定理中证明，这类谓词在算术中是可定义的（递归的），但“公式n可证”这一命题（∃m Proof(m, n)）不可在系统内被证明一致。

6. 应用与意义

   • 哥德尔不完备定理：通过编码构造自指命题“本语句不可证”，揭示形式系统的不完备性。
   • 计算理论：编码是递归函数论的基础，展示了形式化与可计算性的深刻联系。

通过以上步骤，哥德尔编码将逻辑的句法转化为算术对象，为元数学提供了严格的数学基础。