2026-08-25 · 把元证明送回算术内部

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

前两日已经完成两件事：先用对角引理造出

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

再从理论外部证明：若 $T$ 一致，则 $T⊬G_T$。今天的 originating problem（起始问题）是：能否把这段外部论证本身编码成 $T$ 内的一条蕴含？ 若能，外部假设“$T$ 一致”就会对应对象语言中的算术句 $\mathrm{Con}(T)$，而第一不完备定理便会反过来限制 $T$ 对自己的认证能力。

对象与量词分四层：

1. 元语言中的理论 $T$、外部判断 $T⊢A$ 与元意义一致性；
2. 自然数上的有限证明码 $p$，以及可计算的证明拼接、引用和核验函数；
3. 对象语言中的 ${\mathrm{Prf}}_T(p,q)$、${\mathrm{Prov}}_T(q)$ 与 $\mathrm{Con}(T)$；
4. $T$ 内部对这些算术公式的证明，例如 $T⊢{\mathrm{Prov}}_T(⌜A⌝)\to {\mathrm{Prov}}_T(⌜{\mathrm{Prov}}_T(⌜A⌝)⌝)$。

这里最易混淆的是第一层与第四层：

$$T⊢A⟹T⊢{\mathrm{Prov}}_T(⌜A⌝)$$

是一条关于所有具体句子 $A$ 的元条件；它不是把“$T⊢$”当作对象语言量词写入 $T$。

先修。 Gödel 编码、证明关系的表示、对角引理、第一不完备定理，以及经典命题逻辑。去向。 Löb theorem（Löb 定理）、provability logic GL（可证性逻辑 GL）、反思原则与序数分析。主导 proof engines 是：把 proof transformation（证明变换）实现为原始递归函数；在弱算术中证明这些函数确实合成有效证明；再把昨日的元层反证压缩为 $T$ 内的 $\mathrm{Con}(T)\to G_T$。

本期是三日 exploration micro-arc 的第 3 日：第 1 日造固定点，第 2 日证明第一不完备并比较 Rosser 改进，今天完成第二不完备定理并说明“哪一种可证性谓词”为什么成为结论的一部分。

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

1.1 标准可证性谓词为何不只是“定理集合”

固定算术语言中的理论 $T$，并作如下明确假设：

• $T$ 一致且递归可公理化；
• $T$ 包含足以形式化有限句法与证明码运算的基础算术，例如 $I{\mathrm{\Sigma }}_1$；特别地，任何满足这些条件的 $\mathrm{PA}$ 扩张都属于此框架；
• 选定一个标准 proof predicate（证明谓词）${\mathrm{Prf}}_T(p,q)$，并定义
  $${◻}_{T}A:⟺{\mathrm{Prov}}_T(⌜A⌝):⟺\mathrm{\exists }p{\mathrm{Prf}}_T(p,⌜A⌝).$$

下文常把 ${◻}_{T}A$ 简写成 $◻A$。相应的 canonical consistency statement（标准一致性句）是

$$\mathrm{Con}(T):⟺\mathrm{\neg }◻\mathrm{\perp },\mathrm{\perp }\equiv (0=1).$$

对标准 ${\mathrm{\Sigma }}_1^0$ 可证性谓词，下面三条 Hilbert–Bernays–Löb derivability conditions（Hilbert–Bernays–Löb 可导条件）成立；这里 $A,B$ 遍历 $T$ 的句子：

1. HBL1 / necessitation meta-condition（必然化元条件）
   $$\mathrm{\forall }A\in \mathrm{Sent}(T),T⊢A⟹T⊢◻A.$$
2. HBL2 / internalized modus ponens（内化 modus ponens）
   $$\mathrm{\forall }A,B\in \mathrm{Sent}(T),T⊢◻(A\to B)\to (◻A\to ◻B).$$
3. HBL3 / positive introspection（正内省）
   $$\mathrm{\forall }A\in \mathrm{Sent}(T),T⊢◻A\to ◻◻A.$$

这些条件不是把“证明很可信”当作公理。HBL1 来自：给定一份有限 $T$-证明，可以计算其标准编号并在 $T$ 中核验。HBL2 来自一个原始递归函数，它把 $A\to B$ 的证明码和 $A$ 的证明码拼成 $B$ 的证明码。HBL3 则把一份证明码 $p$ 转成一份证明“存在证明码 $p$”的证明码。第二不完备定理所需的额外算术强度，正用于在 $T$ 内统一证明这些 code transformers（编码变换器）正确，而不只是对每个外部给定编号逐个核验。[1][2]

1.2 把第一不完备定理内化

由对角引理，取标准 Gödel sentence（Gödel 句）$G_T$，使

$$\begin{array}{}\text{(G)}& T⊢G_T\leftrightarrow \mathrm{\neg }◻G_T.\end{array}$$

先证明

$$\begin{array}{}\text{(1)}& T⊢G_T\to \mathrm{Con}(T).\end{array}$$

因为 $T$ 证明命题逻辑重言式 $\mathrm{\perp }\to G_T$，由 HBL1 与 HBL2，

$$T⊢◻\mathrm{\perp }\to ◻G_T.$$

取逆否命题得到

$$T⊢\mathrm{\neg }◻G_T\to \mathrm{\neg }◻\mathrm{\perp }.$$

再由 $(G)$ 的 $G_T\to \mathrm{\neg }◻G_T$ 方向，即得 $(1)$。

关键的另一方向是

$$\begin{array}{}\text{(2)}& T⊢\mathrm{Con}(T)\to G_T.\end{array}$$

由 $(G)$，$T$ 证明 $G_T\to \mathrm{\neg }◻G_T$。HBL1 先把这条定理引用进可证性谓词，HBL2 再给出

$$\begin{array}{}\text{(3)}& T⊢◻G_T\to ◻\mathrm{\neg }◻G_T.\end{array}$$

另一方面，HBL3 给出

$$\begin{array}{}\text{(4)}& T⊢◻G_T\to ◻◻G_T.\end{array}$$

若同时有一份 $◻G_T$ 的证明和一份 $\mathrm{\neg }◻G_T$ 的证明，标准证明合成器便能产生 $\mathrm{\perp }$ 的证明。把这一步用 HBL2 形式化，并合并 $(3)$、$(4)$，得到

$$T⊢◻G_T\to ◻\mathrm{\perp }.$$

逆否后为

$$T⊢\mathrm{\neg }◻\mathrm{\perp }\to \mathrm{\neg }◻G_T.$$

再由 $(G)$ 的 $\mathrm{\neg }◻G_T\to G_T$ 方向，得到 $(2)$。因此，针对这个标准证明谓词，$T$ 内部实际上证明

$$\begin{array}{}\text{(5)}& T⊢G_T\leftrightarrow \mathrm{Con}(T).\end{array}$$

这不是说两个字符串相同，而是说：当第一不完备定理的证明变换都被内化以后，“这个 Gödel 句不可证”与“没有 $T$-矛盾证明”在 $T$ 内可证等价。[1]

1.3 Gödel 第二不完备定理

定理（Gödel Second Incompleteness Theorem，Gödel 第二不完备定理；标准形式）。 对每个句法可有效编码、满足上述可导条件的递归可公理化理论 $T$，

$${\mathrm{Con}}_{\mathrm{meta}}(T)⟹T⊬\mathrm{Con}(T).$$

证明。 反设 $T⊢\mathrm{Con}(T)$。由 $(2)$ 与 modus ponens，

$$T⊢G_T.$$

但第一不完备定理的第一半已经证明：$T$ 一致蕴含 $T⊬G_T$。矛盾。因此 $T⊬\mathrm{Con}(T)$。证毕。

外部假设只需普通一致性；更强的可靠性或 1-一致性并未进入这个反证。代价在别处：与第一定理相比，第二定理必须更细致地固定证明谓词，并要求基础算术能够统一验证 HBL 条件。SEP 的标准综述也提醒：第一定理对很弱的 $Q$ 已成立，而第二定理的常规证明通常采用近似 PRA 或更强的句法形式化能力；过弱理论中的“一致性句是否真的表达一致性”另有细节。[1]

1.4 Graduate / modern extension：Löb 定理与局部反思

对任意句子 $A$，local reflection（局部反思）实例是

$$◻A\to A.$$

Löb 定理把第二不完备的单个边界推广成精确分类：若标准可证性谓词满足 HBL 条件，则

$$T⊢(◻A\to A)⟺T⊢A.$$

从右向左是命题逻辑；真正的内容是左向右。令 $A=\mathrm{\perp }$，则 $◻\mathrm{\perp }\to \mathrm{\perp }$ 正是 $\mathrm{\neg }◻\mathrm{\perp }$，所以一致的 $T$ 若证明自身一致性，Löb 定理会迫使 $T⊢\mathrm{\perp }$。第二不完备定理由此成为 Löb 定理的 $A=\mathrm{\perp }$ 特例。[2]

把 $◻$ 抽象成模态算子，HBL2 对应 distribution axiom，HBL1 对应 necessitation rule，Löb 定理对应

$$◻(◻A\to A)\to ◻A.$$

这生成 provability logic GL。于是本微弧从一个算术固定点出发，最后抵达一门研究“理论如何谈论自身证明”的模态逻辑；Solovay 的算术完备性进一步说明，GL 精确捕捉了 PA 关于标准可证性谓词的命题模态原则。[2]

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

题目

设 $(\mathrm{\Omega },\mathcal{F},\mathbb{P})$ 为概率空间，$X_n:\mathrm{\Omega }\to \mathbb{R}$ 为随机变量。假设存在常数 $p>0$、$\alpha >0$ 与 $C<\mathrm{\infty }$，使

$$\mathrm{\forall }n\ge 1,\mathbb{E}|X_n{|}^p\le \frac{C}{n^{1+\alpha }}.$$

证明

$$X_n⟶0\mathbb{P}\text{-a.s.}$$

并指出证明中是否需要随机变量之间相互独立。

模板识别

看到“矩估计随 $n$ 可和衰减 + 几乎处处结论”，应识别 moment bound $\to$ tail probability $\to$ first Borel–Cantelli（矩界转尾概率再用第一 Borel–Cantelli）模板。先固定一个阈值，不要直接处理不可数多个 $\epsilon >0$；最后用可数阈值族恢复收敛定义。

分级提示

1. 对固定 $\epsilon >0$，把 Markov inequality（Markov 不等式）用于非负随机变量 $|X_n{|}^p$。
2. 检查级数 $\sum _n\mathbb{P}(|X_n|>\epsilon )$ 是否收敛，并调用第一 Borel–Cantelli 引理。
3. 第一 Borel–Cantelli 只告诉你：对一个固定阈值，超出该阈值的事件只发生有限次。
4. 只对 $\epsilon =1/k$，$k\in {\mathbb{N}}_{>0}$，取可数交；再由任意 $\epsilon >0$ 选取足够大的 $k$。

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

语境。 Gödel 在 1931 年原论文 Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I 的脚注 46 中，不只陈述某个形式系统不完备，还把这种不完备放进“继续加入更高类型”的开放层级。下面德文短引已从 Springer 所呈原文脚注核对。[3]

“Der wahre Grund für die Unvollständigkeit, welche allen formalen Systemen der Mathematik anhaftet, liegt, wie im II. Teil dieser Abhandlung gezeigt werden wird, darin, daß die Bildung immer höherer Typen sich ins Transfinite fortsetzen läßt.”

“一切数学形式系统之所以不完备，其真正原因——按作者当时计划在论文第二部分中说明的说法——在于更高类型的形成可以向超限层级不断推进。”

释义（paraphrase）。 Gödel 紧接着指出，给当前系统加入适当的更高类型，可以判定当前构造出的不可判定句；但新的扩张仍会产生自己的限制。这里显出的数学态度不是把“不完备”理解为研究停止，而是把它理解为 strength progression（强度递进）：解决旧障碍的原则成为新系统的一部分，新系统再接受新的元数学审计。

今天的现代形式是反思阶梯：$T$ 不能证明标准 $\mathrm{Con}(T)$，但更强的 $T+\mathrm{Con}(T)$ 把它收入公理；随后又出现 $\mathrm{Con}(T+\mathrm{Con}(T))$。原文的高阶类型解释、后来的反思原则与 proof-theoretic ordinal（证明论序数）不是同一个形式体系，不能直接等同；它们共享的结构性眼光是：基础强化可以有秩序地迭代，却不存在由第二不完备定理认可的有限终极自证层。

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

外部同延不够：Rosser“一致性”反而可在内部证明

昨日定义过 Rosser provability predicate（Rosser 可证性谓词）：

$${\mathrm{RProv}}_T(x):⟺\mathrm{\exists }p({\mathrm{Prf}}_T(p,x)\wedge \mathrm{\forall }q<p\mathrm{\neg }{\mathrm{Prf}}_T(q,\mathrm{Neg}(x))).$$

若 $T$ 在元意义下一致，则对每个标准句子 $A$，普通可证性与 Rosser 可证性在标准模型中选出相同的句子。然而，把一致性改写成

$$\mathrm{RCon}(T):⟺\mathrm{\neg }{\mathrm{RProv}}_T(⌜\mathrm{\perp }⌝),$$

会出现与第二不完备定理完全不同的行为：对通常的 Rosser 谓词，一致的 $T$ 可以证明 $\mathrm{RCon}(T)$。[1]

逐项检查其机制。令 $\mathrm{\perp }$ 为 $0=1$，并固定一份 $T$ 对 $\mathrm{\neg }\mathrm{\perp }$ 的标准证明，其编号为 $q_0$。

1. 若 $p>q_0$，则 $q_0<p$ 本身就是一份更早的 $\mathrm{\neg }\mathrm{\perp }$ 证明；所以 $p$ 不可能满足 Rosser 谓词中的“此前没有反证明”。
2. 只剩有限多个 $p\le q_0$。元层的一致性保证它们都不是 $\mathrm{\perp }$ 的真正证明码。
3. proof checking 是可判定关系；因此对这有限多个具体编号，$T$ 能逐一证明
   $$\mathrm{\neg }{\mathrm{Prf}}_T(\overline{p},⌜\mathrm{\perp }⌝).$$
4. 把有限低编号核验与第 1 项合并，$T$ 便证明不存在赢得“早于反证明”竞赛的 $\mathrm{\perp }$ 证明，即
   $$T⊢\mathrm{RCon}(T).$$

这没有反驳第二不完备定理。暴露的边界恰是：

$$\text{外部同延}⟹⧸\phantom{⟹}\text{内部可替换}.$$

标准 ${\mathrm{Prov}}_T$ 记录可组合、可再次引用的普通证明；Rosser 谓词额外依赖“与相反证明比较编号”的非单调条件，通常不能保留第二定理所需的全部 HBL 行为。故第二不完备定理不是关于任意一个在 $\mathbb{N}$ 中恰好枚举 $T$ 定理的公式，而是关于适当表示标准证明机制的可证性谓词。这是一个 intensional theorem（内涵性定理）。[1][2]

附近另一个必须保留的边界是：定理不禁止更强理论证明较弱理论的一致性。$T+\mathrm{Con}(T)$ 按定义证明 $\mathrm{Con}(T)$；若该扩张一致，第二定理限制的是它对自身标准一致性句 $\mathrm{Con}(T+\mathrm{Con}(T))$ 的证明。

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

今日一问。 从一个满足本期假设的基础理论 $T_0$ 出发，递归定义

$$T_{n+1}=T_n+\mathrm{Con}(T_n),T_{\omega }=\bigcup _{n<\omega }{T}_n.$$

假设外部元理论确认每个 $T_n$ 一致，并且这一理论序列及其证明谓词都被有效地统一编码。请审计下列三件事：

1. 为什么 $T_{n+1}$ 证明 $\mathrm{Con}(T_n)$，却仍不能证明 $\mathrm{Con}(T_{n+1})$？
2. 为什么 $T_{\omega }$ 包含每个有限层的一致性句，却不能仅凭这一事实就宣称它证明自己的标准 $\mathrm{Con}(T_{\omega })$？
3. “任意 $T_{\omega }$-证明只使用有限多个公理”这一外部事实，要变成 $T_{\omega }$ 内的一致性证明，还缺少哪一种统一反思或归纳能力？

方向提示。 分清

$$\mathrm{\forall }n\in \mathbb{N},T_{\omega }⊢\mathrm{Con}(T_n)$$

与对象语言中的一个统一全称句；还要重新检查 $T_{\omega }$ 是否递归可公理化、其标准证明谓词是否满足 HBL 条件。不要把“每个固定有限层都已处理”无条件交换成“整个有效并层已经处理”。

数学地图。 三日主线闭合为

$$\text{有效句法编码}⟶\text{对角固定点}⟶\text{第一不完备}⟶\text{HBL 可导条件}⟶\mathrm{Con}(T)\leftrightarrow G_T⟶\text{第二不完备}.$$

向模态逻辑一侧：

$$\text{HBL 条件}⟶\text{Löb 定理}⟶\text{GL}⟶\text{Solovay 算术完备性}.$$

向证明论一侧：

$$T⟶T+\mathrm{Con}(T)⟶\text{迭代反思}⟶\text{超限递进}⟶\text{序数分析}.$$

Gentzen 对 PA 的一致性证明使用超出 PA 内部可证范围的超限归纳，这正是“更强外部原则可以证明较弱系统一致性”的典型去向；第二不完备定理限制自证，不禁止有明确强度账本的相对一致性证明。[1]

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

展开完整解答

模板：矩界 $\to$ Markov 尾界 $\to$ 第一 Borel–Cantelli $\to$ 可数阈值对角化。

固定任意整数 $k\ge 1$，并令

$$A_{n,k}=\{|X_n|>1/k\}.$$

对非负随机变量 $|X_n{|}^p$ 应用 Markov 不等式：

$$\begin{array}{rl}\mathbb{P}(A_{n,k})& =\mathbb{P}(|X_n{|}^p>k^{-p})\\ & \le k^p\mathbb{E}|X_n{|}^p\\ & \le C{k}^p{n}^{-(1+\alpha )}.\end{array}$$

因为 $\alpha >0$，$p$-级数判别给出

$$\sum _{n=1}^{\mathrm{\infty }}{n}^{-(1+\alpha )}<\mathrm{\infty }.$$

所以对每个固定 $k\ge 1$，

$$\sum _{n=1}^{\mathrm{\infty }}\mathbb{P}(A_{n,k})\le C{k}^p\sum _{n=1}^{\mathrm{\infty }}{n}^{-(1+\alpha )}<\mathrm{\infty }.$$

由第一 Borel–Cantelli 引理，

$$\mathbb{P}(A_{n,k}\mathrm{i}.\mathrm{o}.)=0,$$

其中

$$A_{n,k}\mathrm{i}.\mathrm{o}.=\bigcap _{N=1}^{\mathrm{\infty }}\bigcup _{n\ge N}{A}_{n,k}$$

表示事件 $|X_n|>1/k$ 发生无穷多次。等价地，存在概率为 $1$ 的事件 $E_k$，使对每个 $\omega \in E_k$，存在整数 $N_k=N_k(\omega )$ 满足

$$\mathrm{\forall }n\ge N_k,|X_n(\omega )|\le 1/k.$$

现在取可数交

$$E=\bigcap _{k=1}^{\mathrm{\infty }}{E}_k.$$

因为每个 $\mathbb{P}(E_k)=1$，可数次可加性给出 $\mathbb{P}(E)=1$。固定 $\omega \in E$ 与任意 $\epsilon >0$。选择 $k$ 使 $1/k<\epsilon$；由 $\omega \in E_k$，存在 $N_k(\omega )$，使所有 $n\ge N_k(\omega )$ 都满足

$$|X_n(\omega )|\le 1/k<\epsilon .$$

因此 $X_n(\omega )\to 0$。这对所有 $\omega \in E$ 成立，而 $\mathbb{P}(E)=1$，故

$$X_n\to 0\mathbb{P}\text{-a.s.}$$

证明只使用第一 Borel–Cantelli 引理；该方向不要求事件 $A_{n,k}$ 独立，因此也不要求随机变量 $(X_n)$ 相互独立。独立性通常出现在第二 Borel–Cantelli 引理从概率级数发散推出“无穷多次发生”的方向。

复用这个模板时应保留四步：用矩界生成尾概率界；验证概率级数可和；对每个固定阈值排除 limsup 事件；最后只对一个可数且趋零的阈值族取交。

资料与来源 (Sources)

1. Stanford Encyclopedia of Philosophy, “Gödel’s Incompleteness Theorems,” 尤见 §§1.2.1、3.1–3.3、4.3：第二定理的标准假设、$\mathrm{Con}(T)$ 的形式化、可导条件、Rosser 谓词的内涵边界、反思原则与 Gentzen 去向。https://plato.stanford.edu/entries/goedel-incompleteness/
2. Stanford Encyclopedia of Philosophy, “Provability Logic,” 尤见 §§1、2.2、4.1–4.2：Löb 条件、Löb 定理、GL 公理、第二不完备定理的模态特例与 Solovay 算术完备性。https://plato.stanford.edu/entries/logic-provability/
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 节短引核自 Springer 页面所呈脚注 46。https://link.springer.com/article/10.1007/BF01700692