2026-08-22 · 让公式指向自己的编号

0. 导读与元结构 (Orientation & Meta-structure)

形式系统只能按规则操作符号；“这个句子谈论自己”却像是在系统外部替句子配了一面镜子。真正的问题是：一个算术公式如何在不新增“引用”原语的情况下，获得关于自身句法的可证明陈述？

今天把对象分成四层：

1. 元语言中的有限字符串，例如公式 $\phi (x)$；
2. 元语言中的自然数 $⌜\phi ⌝\in \mathbb{N}$，即公式的 Gödel number（Gödel 编号）；
3. 对象语言中的数词 $\overline{⌜\phi ⌝}$，它在标准模型中表示上述自然数；
4. 理论 $T$ 内的可证关系 $T⊢\sigma$。

三者绝不能混型：公式不是自然数，自然数也不是对象语言中的字符串；把元句法编码成数，再用数词送回对象语言，才形成闭环。为减轻记号，后文按惯例把 $A(\overline{⌜D⌝})$ 简写为 $A(⌜D⌝)$，但这个横线所表示的类型转换始终存在。

先修：一阶公式、自由变量与代入，自然数的原始递归函数，以及“$T⊢\phi$”的元语言含义。去向：Gödel 第一定理与第二不完备定理、Tarski 真不可定义定理、Löb 定理和 provability logic（可证性逻辑）。主导 proof engines 是有效编码、句法操作的原始递归性、在弱算术中的可表示性，以及一次精确的“把代码输入给自身”的对角代入。

这是三日 exploration micro-arc 的第 1 日。今天只造发动机——对角引理；第 2 日才把 $A(x)$ 取成“编号 $x$ 的句子不可证”，并审计不可证与不可否证分别需要什么假设；第 3 日再把证明过程内化，进入一致性陈述与第二不完备定理。

1. 核心概念、定理与谱系 (Concept, Theorem & Lineage)

1.1 从有限句法到自然数运算

固定一阶算术语言 $L_A=\{0,S,+,\times ,=\}$，并固定一种 effective Gödel numbering（有效 Gödel 编号）：每个 $L_A$-项、公式与有限推导都获得一个自然数代码，而且下列元句法判定与操作在代码上是原始递归的：

• $\mathrm{Fml}(n)$：$n$ 是否为公式代码；
• $\mathrm{Sent}(n)$：$n$ 是否为句子代码；
• $\mathrm{Neg}(n)$：从公式代码得到其否定的代码；
• $\mathrm{Sub}(e,n)$：若 $e$ 编码一个指定自由变量为 $x$ 的公式，就把数词 $\overline{n}$ 代入 $x$，输出所得公式的代码。

对非法输入可任取一个默认输出，使这些函数在 $\mathbb{N}$ 上全定义；这不会影响后面只对合法公式代码的使用。编码的具体质因数方案并不重要，重要的是“编码、识别、拼接、代入”都能由有限机械步骤完成。[1]

设 $Q$ 为 Robinson arithmetic（Robinson 算术）。今天只用它的一个关键能力：每个原始递归函数都可在 $Q$ 中用算术公式 numeralwise represent（逐数词表示），并可选取表示使正确输出对固定输入具有可证明的唯一性。具体到 $\mathrm{Sub}$，存在公式 $S(u,v,w)$，使得对所有 $e,n,m\in \mathbb{N}$，若 $\mathrm{Sub}(e,n)=m$，则

$$Q⊢\mathrm{\forall }w(S(\overline{e},\overline{n},w)\leftrightarrow w=\overline{m}).$$

这里 $S$ 是对象语言中的三元算术公式；$\mathrm{Sub}$ 是元语言中的自然数函数。可表示性正是两层之间的接口。

1.2 对角引理：完整量词与构造

定理（Diagonal Lemma / Fixed-point Lemma，对角引理 / 固定点引理）。 设 $T$ 是算术语言中的任意一阶理论，且 $Q\subseteq T$。则

$$\mathrm{\forall }A(x)\in \mathrm{Fml}(L_A),(\mathrm{FV}(A)\subseteq \{x\})⟹\mathrm{\exists }D\in \mathrm{Sent}(L_A),T⊢D\leftrightarrow A(⌜D⌝).$$

其中 $A(⌜D⌝)$ 是 $A(\overline{⌜D⌝})$ 的简写。定理不假设 $T$ 一致，也不假设 $T$ 的公理可判定；这些假设在把固定点用于“$T$ 内的可证性谓词”时才进入。

证明。 固定只有变量 $x$ 可能自由出现的公式 $A(x)$。利用上节表示代入的公式 $S$，定义另一个一元公式

$$B(x):⟺\mathrm{\exists }y(S(x,x,y)\wedge A(y)).$$

令

$$b=⌜B(x)⌝,D=B(\overline{b}),d=⌜D⌝.$$

按 $D$ 的定义，$d$ 恰是把 $B$ 的代码 $b$ 输入给其自身自由变量所得句子的代码，即

$$d=\mathrm{Sub}(b,b).$$

由 $S$ 对 $\mathrm{Sub}$ 的带唯一性表示，

$$Q⊢\mathrm{\forall }y(S(\overline{b},\overline{b},y)\leftrightarrow y=\overline{d}).$$

又因 $Q\subseteq T$，同一公式在 $T$ 中可证。于是

$$\begin{array}{rl}T& ⊢D\leftrightarrow B(\overline{b})\\ & \leftrightarrow \mathrm{\exists }y(S(\overline{b},\overline{b},y)\wedge A(y))\\ & \leftrightarrow \mathrm{\exists }y(y=\overline{d}\wedge A(y))\\ & \leftrightarrow A(\overline{d})\\ & \leftrightarrow A(⌜D⌝).\end{array}$$

证毕。[2]

证明中真正的“对角”只有一步：把 $B$ 的代码 $b$ 同时放进 $\mathrm{Sub}$ 的公式代码槽与代入数值槽。句子 $D$ 不是凭空写下的语义悖论，而是由可计算代入操作机械产生的固定点。

1.3 为什么这会通向不完备性

若 $T$ 还是 recursively axiomatizable（递归可公理化）的，并含有足够的初等算术，则“$p$ 编码一份 $T$-证明，其末行代码为 $q$”可被算术公式 ${\mathrm{Prf}}_T(p,q)$ 表示。定义 provability predicate（可证性谓词）

$${\mathrm{Prov}}_T(q):⟺\mathrm{\exists }p{\mathrm{Prf}}_T(p,q).$$

把对角引理应用于

$$A(x)=\mathrm{\neg }{\mathrm{Prov}}_T(x),$$

就得到一个句子 $G_T$，满足

$$T⊢G_T\leftrightarrow \mathrm{\neg }{\mathrm{Prov}}_T(⌜G_T⌝).$$

这只是构造固定点，还不是不完备定理。要从中推出 $T⊬G_T$，必须把“外部确有一份 $T$-证明”转成“$T$ 内证明其代码满足 ${\mathrm{Prov}}_T$”，并使用 $T$ 的一致性；要推出 $T⊬\mathrm{\neg }{G}_T$，Gödel 原证明还需要更强的 $\omega$-一致性或相应的 1-一致性条件，Rosser 才把第一定理的假设降到普通一致性。明日将逐步分账。

谱系与现代延伸。 Gödel 1931 年的原论文为形式表达式与证明配置自然数代码，再让元数学关系进入算术；现代教材通常把其中反复出现的替换机制抽离成上面的对角引理。[1][3] 同一固定点机器并不限于“不可能证明”：把 $A(x)$ 换成含可证性谓词的其他公式，会导向 Löb 定理；把“程序作用于自己的代码”放到可计算函数世界，则与 Kleene recursion theorem（Kleene 递归定理）形成平行结构。共同机制不是含混的“自我意识”，而是有效表示系统拥有可执行的 quotation-plus-substitution（引用加代入）接口。

2. 固定模板习题 (Template Exercise)

题目

设 $X$ 为任意集合，$f:X\to \mathcal{P}(X)$ 为任意函数。证明 $f$ 不可能为满射。亦即证明

$$\mathrm{\forall }X\mathrm{\forall }f:X\to \mathcal{P}(X),\mathrm{\exists }D\subseteq X,\mathrm{\forall }a\in X,f(a)\ne D.$$

模板识别

信号是“把每个索引 $x$ 配给一个关于 $x$ 的对象 $f(x)$，并要求构造一个不在像中的对象”。遇到这类 surjectivity obstruction（满射障碍），尝试在第 $x$ 个位置故意与 $f(x)$ 相反；这就是 diagonal anti-surjection（对角反满射）模板。

分级提示

1. 新集合 $D$ 必须是 $X$ 的子集；请用一个关于“$x$ 是否属于 $f(x)$”的谓词定义它。
2. 令 $D=\{x\in X:x\notin f(x)\}$。
3. 若 $f$ 满射，则存在 $a\in X$ 使 $f(a)=D$；只检查元素 $a$ 自己是否属于这两个集合。
4. 把定义和 $f(a)=D$ 并列，会得到 $a\in D\leftrightarrow a\notin D$。

3. 大家之言 (Mathematician in Their Own Words)

语境。 Kurt Gödel 在 1931 年发表于 Monatshefte für Mathematik und Physik 的论文 Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I 中，于脚注 14 专门解释所构造的不可判定句为何不是循环论证。本文已按 Springer 的原文页面核对下面这句短引。[3]

“Ein solcher Satz hat entgegen dem Anschein nichts Zirkelhaftes an sich, denn er behauptet zunächst die Unbeweisbarkeit einer ganz bestimmten Formel”

“这样的命题虽表面如此，实则并无循环性，因为它首先断言某个完全特定的公式不可证。”

释义（paraphrase）。 Gödel 随后说明：该句首先断言某个完全特定的公式不可证；只有在构造完成以后，才发现被谈论的公式恰好就是表达该断言的公式本身。

这段话揭示的不是一般性的“大胆自指”，而是一条严格方法论：先在元语言中指定代码与代入操作，证明所得对象满足形式等价式，最后才允许用“它谈论自己”作直观简称。换言之，解释应当追随 construction（构造），不可取代 construction。今天证明里的 $b\mapsto \mathrm{Sub}(b,b)$ 正是消除循环疑虑的技术核心。

4. 反例与边界 (Counterexample & Boundary)

4.1 对角引理本身不产生独立命题

取

$$T_{\mathrm{\perp }}=Q+(0=1).$$

逐项检查：

1. $T_{\mathrm{\perp }}$ 扩张 $Q$，所以第 1 节的句法编码与对角引理仍适用；
2. $T_{\mathrm{\perp }}$ 不一致，因为 $Q⊢0\ne 1$，而新增公理给出 $0=1$；
3. 在经典逻辑中，由矛盾可推出任意句子，故对每个句子 $\sigma$，都有
   $$T_{\mathrm{\perp }}⊢\sigma \text{且}{T}_{\mathrm{\perp }}⊢\mathrm{\neg }\sigma .$$
4. 因而即使对角引理构造出
   $$T_{\mathrm{\perp }}⊢G\leftrightarrow \mathrm{\neg }{\mathrm{Prov}}_{T_{\mathrm{\perp }}}(⌜G⌝),$$
   也绝无“$G$ 既不可证又不可否证”的结论。

暴露的边界是：固定点机制不要求一致性；从固定点到独立性才要求一致性。 把二者合并成一句“自指导致不可证”会丢掉真正的证明依赖。

4.2 “递归可公理化”本身也不推出不完备

Presburger arithmetic（Presburger 算术）研究标准自然数中的加法一阶理论。它具有下列性质：[1]

1. 有标准模型 $(\mathbb{N};0,1,+,<)$，故一致；
2. 可判定，因而其定理集可递归枚举；
3. 完备：对语言中的每个句子 $\sigma$，理论证明 $\sigma$ 或证明 $\mathrm{\neg }\sigma$；
4. 它不具备含乘法的 Robinson 算术 $Q$ 所提供的标准算术强度，因此第 1 节所调用的“在 $Q$ 中表示所需句法函数”这一充分条件并不成立。

所以附近的错误命题

“每个一致且递归可公理化的无限理论都不完备”

被 Presburger 算术直接否定。Gödel 不完备性的适用条件不是形式系统“很大”或对象“无限”，而是系统能在内部承载足够的自然数算术，尤其能把证明检查和对角代入转成可表示的数论关系。

最后再校准一句常见简称：对角引理给的是

$$T⊢D\leftrightarrow A(⌜D⌝),$$

不是字符串恒等式

$$D=A(⌜D⌝).$$

左式是理论内可证等价；右式若被理解成两个公式逐字符相同，通常既非构造目标，也非证明所需。把 material equivalence（实质等价）误读成意义或字符串同一，正是“循环悖论”错觉的来源之一。[1]

5. 今日一问与数学地图 (Question & Map)

今日一问。 设 $T$ 是一致、递归可公理化且包含 $Q$ 的理论；令 $G_T$ 满足

$$T⊢G_T\leftrightarrow \mathrm{\neg }{\mathrm{Prov}}_T(⌜G_T⌝).$$

请把下面两个目标分开审计：

$$T⊬G_T,T⊬\mathrm{\neg }{G}_T.$$

为什么第一个目标只需普通一致性，而沿 Gödel 原谓词证明第二个目标时会碰到更强的 1-一致性障碍？如果把“某命题有证明”改成“它有一份早于其否定之任何证明的证明”，Rosser 的证明次序比较可能在哪一步消除这项障碍？

方向提示。 对第一式，暂时假设 $T⊢G_T$，把这份外部证明的具体代码送入 ${\mathrm{Prf}}_T$；对第二式，不要把“$T$ 没有证明”误写成“$T$ 证明没有证明”，而要追踪一个存在量词式可证性陈述何时可能在标准模型中为假。

数学地图。 路线为

$$\text{有限字符串}⟶\text{Gödel 编码}⟶\text{原始递归句法}⟶\text{算术可表示性}⟶\text{对角固定点}⟶\text{第一不完备定理}.$$

向一侧走，真谓词的固定点导向 Tarski undefinability（Tarski 不可定义性）；向另一侧走，把“可证性对蕴含封闭”等事实在 $T$ 内形式化，导向 Hilbert–Bernays–Löb derivability conditions（可导条件）、第二不完备定理与可证性逻辑。模型论方向则追问：为何非标准自然数会在某些模型中充当“非标准长度证明”的代码。

附录 A：习题完整解答 (Full Solution)

展开完整解答

模板：对角反满射 (diagonal anti-surjection)。

给定任意集合 $X$ 与任意函数 $f:X\to \mathcal{P}(X)$，定义

$$D=\{x\in X:x\notin f(x)\}.$$

这个定义逐项决定 $D$ 的成员，所以 $D\subseteq X$，即 $D\in \mathcal{P}(X)$。

下面证明 $D$ 不在 $f$ 的像中。反设存在 $a\in X$ 使

$$f(a)=D.$$

由 $D$ 的定义，取 $x=a$，得到

$$a\in D⟺a\notin f(a).$$

再用 $f(a)=D$ 代换右侧，便有

$$a\in D⟺a\notin D,$$

矛盾。因此

$$\mathrm{\forall }a\in X,f(a)\ne D.$$

于是 $f$ 不是满射。由于 $X$ 与 $f$ 均任意，得到

$$\mathrm{\forall }X\mathrm{\forall }f:X\to \mathcal{P}(X),f\text{ 不是满射}.$$

复用该模板时应识别三步：按索引构造“相反坐标”的对象；假设它等于某个被枚举对象；在该对象自己的索引处制造双条件矛盾。与第 1 节相比，Cantor 证明在成员关系上翻转对角项；Gödel 构造则先把代入操作编码进算术，再让公式代码成为自己的输入。二者共享对角机制，但对象类型与结论不可混同。

资料与来源 (Sources)

1. Stanford Encyclopedia of Philosophy, “Gödel’s Incompleteness Theorems,” 尤见 §§1.2.3、2.2–2.5：形式理论的条件、可表示性、句法算术化、对角引理、Presburger 边界与第一定理。https://plato.stanford.edu/entries/goedel-incompleteness/
2. Stanford Encyclopedia of Philosophy, supplement “The Diagonalization Lemma”：以代入函数表示公式构造 $B$ 与固定点 $D$ 的逐步证明。https://plato.stanford.edu/entries/goedel-incompleteness/sup2.html
3. Kurt Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik und Physik 38(1), 173–198 (1931), DOI 10.1007/BF01700692；第 3 节短引核自该页面所呈脚注 14。https://link.springer.com/article/10.1007/BF01700692