2026-08-23 · 让证明编号彼此赛跑

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

昨日已经得到固定点

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

但“$G_T$ 说自己不可证”还不是不完备定理。真正的 originating failure（起始失败）是：从理论外部看不到证明，与理论内部证明“不存在证明”，不是同一件事。 前者是元数学事实，后者是一个算术句子；若把二者偷换，便会把普通一致性、1-一致性乃至可靠性混为一谈。

今天的对象分四层：

1. 一个有效公理化、包含 Robinson 算术 $Q$ 的理论 $T$；
2. 标准自然数中的 proof code（证明编号）$p\in \mathbb{N}$；
3. 对象语言公式 ${\mathrm{Prf}}_T(p,q)$ 与 ${\mathrm{Prov}}_T(q)$；
4. 元语言判断 $T⊢\sigma$、$T⊬\sigma$ 与 $\mathbb{N}\models \sigma$。

量词危险集中在

$$\mathrm{\exists }p{\mathrm{Prf}}_T(p,⌜G_T⌝).$$

“每个标准数 $\overline{n}$ 都不是见证”不自动等于“$T$ 能证明不存在任何见证”；$T$ 的非标准模型还可能把某个非标准元素当作一份“非标准长度证明”。Rosser 的关键改造，是不再接受一个无界存在断言，而把正、反证明的编号放进同一场有界先后竞赛。

先修。 昨日的 Gödel 编码、证明关系的可表示性和对角引理；再加经典一阶逻辑中的一致性与演绎定理。去向。 第三日将把外部证明变换内化为 Hilbert–Bernays–Löb derivability conditions（可导条件），进入 $\mathrm{Con}(T)$ 与第二不完备定理。

主导 proof engines 是：从一份具体证明抽取标准编号、逐数词核验原始递归关系、拆开普通一致性与 1-一致性，以及 Rosser 的最小／较早证明比较。本期是三日 exploration micro-arc 的第 2 日：第 1 日造固定点机器，今天用它完成第一不完备定理，第 3 日再问理论为何不能用同一台机器认证自身一致性。

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

1.1 可证性谓词与三种一致性强度

固定一个一阶算术理论 $T$，满足：

• $Q\subseteq T$；
• $T$ 有效公理化，使“$p$ 是 $T$ 中以代码 $q$ 的公式为末行的一份证明”成为可判定关系；
• 所选 Gödel 编码使该关系由算术公式 ${\mathrm{Prf}}_T(p,q)$ 逐数词强表示。

定义标准 provability predicate（可证性谓词）

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

它可取为 ${\mathrm{\Sigma }}_1^0$ 公式。于是对每个句子 $\sigma$，

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

因为外部的一份有限证明有具体标准编号，而 $Q$ 能核验这个编号。[1]

下面把三个假设严格分开。

普通一致性 (consistency)。

$${\mathrm{Con}}_{\mathrm{meta}}(T):⟺\mathrm{\forall }\sigma \in \mathrm{Sent}(T),\mathrm{\neg }(T⊢\sigma \wedge T⊢\mathrm{\neg }\sigma ).$$

$\omega$-一致性 ($\omega$-consistency)。 对每个至多以 $x$ 为自由变量的公式 $A(x)$，不允许同时发生

$$T⊢\mathrm{\exists }xA(x)\text{且}\mathrm{\forall }n\in \mathbb{N},T⊢\mathrm{\neg }A(\overline{n}).$$

1-一致性 (1-consistency)。 只对 ${\mathrm{\Sigma }}_1^0$ 公式施加上面的禁令。等价地，在标准算术解释下，

$$\mathrm{\forall }\theta \in {\mathrm{\Sigma }}_1^0\cap \mathrm{Sent}(T),T⊢\theta ⟹\mathbb{N}\models \theta .$$

因此

$$\omega \text{-一致}⟹1\text{-一致}⟹\text{一致},$$

反向一般不成立。[1] Gödel 1931 年的原始表述使用 $\omega$-一致性；把证明谓词选成 ${\mathrm{\Sigma }}_1^0$ 后，第二半只需 1-一致性。[2]

1.2 Gödel 句：两半证明必须分账

由昨日的对角引理，存在句子 $G_T$，使

$$\begin{array}{}\text{(G)}& T⊢G_T\leftrightarrow \mathrm{\neg }{\mathrm{Prov}}_T(⌜G_T⌝).\end{array}$$

这里的结论分成两个方向。

定理（Gödel 第一定理的原谓词形式）。 设 $T$ 满足上面的有效性与算术强度条件，则：

1. 若 $T$ 一致，则 $T⊬G_T$；
2. 若 $T$ 1-一致，则 $T⊬\mathrm{\neg }{G}_T$。

第一半：一致性排除 $T⊢G_T$。 反设 $T⊢G_T$。取这份证明的标准编号 $n$。证明关系的逐数词可表示性给出

$$T⊢{\mathrm{Prf}}_T(\overline{n},⌜G_T⌝),$$

故

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

另一方面，由 $(G)$ 与 $T⊢G_T$，又有

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

与一致性矛盾。因此 $T⊬G_T$。注意：这里只使用了一份已经给定的有限证明，没有从一个无界存在式中抽取见证。

第二半：1-一致性排除 $T⊢\mathrm{\neg }{G}_T$。 反设 $T⊢\mathrm{\neg }{G}_T$。由 $(G)$ 得

$$\begin{array}{}\text{(1)}& T⊢{\mathrm{Prov}}_T(⌜G_T⌝)\equiv \mathrm{\exists }p{\mathrm{Prf}}_T(p,⌜G_T⌝).\end{array}$$

1-一致性蕴含普通一致性，所以第一半已经给出 $T⊬G_T$。于是没有任何标准自然数 $n$ 真正编码 $G_T$ 的 $T$-证明。由于 proof checking（证明核验）是可判定关系，对每个固定 $n\in \mathbb{N}$，$T$ 都能证明

$$\begin{array}{}\text{(2)}& T⊢\mathrm{\neg }{\mathrm{Prf}}_T(\overline{n},⌜G_T⌝).\end{array}$$

式 $(1)$ 证明一个 ${\mathrm{\Sigma }}_1^0$ 存在句，而式 $(2)$ 排除了它的每个标准见证；这正违反 1-一致性。故 $T⊬\mathrm{\neg }{G}_T$。[1]

这一步的逻辑缺口现在清楚了：普通一致性只禁止 $T$ 同时证明一个句子及其否定，却不禁止 $T$ 证明一个在 $\mathbb{N}$ 中为假的 ${\mathrm{\Sigma }}_1^0$ 存在句。

1.3 Rosser 的改造：让正反证明比较先后

Rosser 不再沿用 $(G)$ 作为最终独立句，而对下面的一元公式应用对角引理：

$$A(x):⟺\mathrm{\forall }p({\mathrm{Prf}}_T(p,x)\to \mathrm{\exists }q<p{\mathrm{Prf}}_T(q,\mathrm{Neg}(x))),$$

其中 $\mathrm{Neg}(x)$ 输出代码 $x$ 所编码公式之否定的代码。得到 Rosser sentence（Rosser 句）$R_T$，满足

$$\begin{array}{}\text{(R)}& T⊢R_T\leftrightarrow \mathrm{\forall }p({\mathrm{Prf}}_T(p,⌜R_T⌝)\to \mathrm{\exists }q<p{\mathrm{Prf}}_T(q,⌜\mathrm{\neg }{R}_T⌝)).\end{array}$$

直观简称是：每一份 $R_T$ 的证明之前，都已经有一份更早的 $\mathrm{\neg }{R}_T$ 证明。 但正式证明只使用 $(R)$。

Rosser 第一定理。 对每个一致、有效公理化且包含 $Q$ 的理论 $T$，都存在句子 $R_T$ 使

$$T⊬R_T\text{且}T⊬\mathrm{\neg }{R}_T.$$

证明架构。

先反设 $T⊢R_T$，并取一份证明的标准编号 $p_0$。理论 $T$ 能核验

$${\mathrm{Prf}}_T({\overline{p}}_0,⌜R_T⌝).$$

由 $(R)$，$T$ 因而证明存在 $q<p_0$ 编码 $\mathrm{\neg }{R}_T$ 的证明。但若 $T$ 一致，实际上没有任何这样的 $q$；而 $q<p_0$ 只涉及有限多个标准候选，$Q$ 能逐一核验并在 $T$ 中否定这个有界存在式，矛盾。故 $T⊬R_T$。

再反设 $T⊢\mathrm{\neg }{R}_T$，取其一份证明的标准编号 $q_0$。对任意证明候选 $p$ 分两段：

• 若 $p\le q_0$，一致性保证 $p$ 不会真是 $R_T$ 的证明；有限核验让 $T$ 证明这一整段没有正证明；
• 若 $p>q_0$，编号 $q_0$ 本身就是一个满足 $q_0<p$ 的反证明见证。

把两段合并，$T$ 证明 $(R)$ 右侧，于是 $T⊢R_T$，与 $T⊢\mathrm{\neg }{R}_T$ 及一致性矛盾。故 $T⊬\mathrm{\neg }{R}_T$。[1][3]

Rosser 改进的核心不是“从存在式神奇地选出最小见证”，而是：一旦反设给出某份具体证明，其编号以下只有有限多个候选；有限真值核验可以在弱算术中完成。 于是原来需要 1-一致性排除的无界假见证，被改造成普通一致性足以控制的有界证明竞赛。

1.4 谱系与现代延伸

Gödel 1931 年的句子使标准可证性谓词作用于自身编号，并以 $\omega$-一致性获得双向不可判定；Rosser 1936 年把正、反证明的次序写进固定点，在稍窄的形式系统框架中把假设降为 simple consistency（普通一致性）。[2][3] 现代的常用版本因而是：

$$\mathrm{\forall }T,[T\text{ 一致、有效公理化且 }Q\subseteq T]⟹\mathrm{\exists }\sigma \in \mathrm{Sent}(T),T⊬\sigma \wedge T⊬\mathrm{\neg }\sigma .$$

这也说明 $Q$ 具有 essential incompleteness（本质不完备性）：任何仍然一致且有效公理化的扩张都无法变成完备理论。

Graduate / modern extension. 在外部、假设 $T$ 一致时，Rosser 可证性与普通可证性对标准句子有相同外延；但第二不完备定理需要的不是外部同延，而是 $T$ 内部可证明的推理闭包与正内省。Rosser 谓词通常不满足所需的全部 derivability conditions。故“它足以改进第一定理”并不意味着“把第二定理中的 ${\mathrm{Prov}}_T$ 机械替换成 Rosser 谓词仍然成立”。这正是明日的入口。[1]

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

题目

设 $f:[0,1]\to [0,1]$ 连续，在 $(0,1)$ 上可微，并存在常数 $q\in [0,1)$ 使

$$\mathrm{\forall }x\in (0,1),|f^{\prime }(x)|\le q.$$

任取 $x_0\in [0,1]$，递归定义 $x_{n+1}=f(x_n)$。证明：

1. $f$ 在 $[0,1]$ 上有唯一不动点 $x_{\ast }$；
2. 对每个 $n\ge 0$，
   $$|x_n-x_{\ast }|\le \frac{q^n}{1-q}|x_1-x_0|;$$
3. 并且
   $$|x_n-x_{\ast }|\le q^n|x_0-x_{\ast }|.$$

模板识别

看到“导数绝对值统一小于 $1$ + 迭代 + 唯一极限”，应识别 contraction iteration（压缩迭代）模板：先用中值定理把导数界变成 Lipschitz 压缩，再估计相邻迭代差，最后用几何级数尾和证明 Cauchy，而不是先猜不动点的显式表达式。

分级提示

1. 先证明对任意 $x,y\in [0,1]$，都有 $|f(x)-f(y)|\le q|x-y|$。
2. 对相邻项应用上式，归纳得到 $|x_{n+1}-x_n|\le q^n|x_1-x_0|$。
3. 对 $m>n$，把 $x_m-x_n$ 写成相邻差的伸缩和，并估计有限几何级数。
4. 得到极限 $x_{\ast }$ 后，用连续性证明 $f(x_{\ast })=x_{\ast }$；唯一性只需把压缩不等式应用于两个不动点。

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

语境。 David Hilbert 在 1900 年巴黎国际数学家大会的 “Mathematical Problems” 演讲中，把算术公理的 compatibility（相容性／一致性）列为第二问题；这里采用 Bulletin of the American Mathematical Society 1902 年刊载、经作者许可并由 Mary Winston Newson 翻译的英文文本。下面短引已从 AMS 原始 PDF 核对。[4]

“To prove that they are not contradictory, that is, that a finite number of logical steps based upon them can never lead to contradictory results.”

“要证明这些公理互不矛盾，也就是说，从它们出发的有限次逻辑步骤永远不会导出相互矛盾的结果。”

释义（paraphrase）。 Hilbert 把一致性问题写成关于有限推导的数学问题：不是诉诸“公理看起来可靠”，而是证明没有任何有限规则链能抵达矛盾。这里已经出现后来 proof theory（证明论）的核心对象——有限形式推导——但 1900 年的讲话早于成熟的 Gödel 编码与今天固定的 $\mathrm{Con}(T)$ 算术句。

这里显出的数学态度是：先把 foundational confidence（基础确信）变成可检查的有限对象问题。Gödel 第二不完备定理将精确限制一种特定方案——一致的充分强理论 $T$ 不能在自身内部证明标准形式的 $\mathrm{Con}(T)$；它并不声称不存在更强理论中的证明，也不否定所有外部、相对的一致性论证。因此，历史谱系应写成“Hilbert 提出并形式化问题方向，Gödel 划定内部方案的边界”，而不是一句“Gödel 证明 Hilbert 错了”。

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

4.1 一致并不蕴含 1-一致：一个条件性纯算术例子

设

$$\mathrm{Con}(\mathrm{PA}):⟺\mathrm{\neg }{\mathrm{Prov}}_{\mathrm{PA}}(⌜0=1⌝),$$

并假设 $\mathrm{PA}$ 在元意义下确实一致。考虑

$$T^{\ast }=\mathrm{PA}+\mathrm{\neg }\mathrm{Con}(\mathrm{PA}).$$

逐项检查：

1. 明日要证明的第二不完备定理给出
   $$\mathrm{PA}⊬\mathrm{Con}(\mathrm{PA}).$$
2. 若 $T^{\ast }$ 不一致，则由演绎定理与经典双重否定，
   $$\mathrm{PA}⊢\mathrm{Con}(\mathrm{PA}),$$
   与第 1 项矛盾。因此 $T^{\ast }$ 一致。
3. 但 $T^{\ast }$ 以公理方式证明
   $$\mathrm{\neg }\mathrm{Con}(\mathrm{PA})\equiv \mathrm{\exists }p{\mathrm{Prf}}_{\mathrm{PA}}(p,⌜0=1⌝).$$
   这是一个 ${\mathrm{\Sigma }}_1^0$ 句子。
4. 因为元层假设 $\mathrm{PA}$ 一致，标准自然数中没有任何 $p$ 编码 $\mathrm{PA}$ 对 $0=1$ 的证明。因此上面的 ${\mathrm{\Sigma }}_1^0$ 句在 $\mathbb{N}$ 中为假。
5. 更具体地，对每个标准 $n\in \mathbb{N}$，proof checking 的可判定性给出
   $$T^{\ast }⊢\mathrm{\neg }{\mathrm{Prf}}_{\mathrm{PA}}(\overline{n},⌜0=1⌝),$$
   同时 $T^{\ast }$ 又证明其存在量化式。

所以，在 $\mathrm{PA}$ 一致这一条件下，$T^{\ast }$ 是一致但非 1-一致的有效公理化算术理论。它的非标准模型可以用非标准元素充当那份虚假的“证明编号”。[1]

这个例子调用第二不完备定理，只作为明日内容的 forward reference（前瞻引用），不参与今天第一不完备定理的证明。它也没有证明 $T^{\ast }$ 恰好否定自己的标准 Gödel 句；它精确证明的是：

$${\mathrm{Con}}_{\mathrm{meta}}(T)⟹⧸\phantom{⟹}1\text{-}\mathrm{Con}(T).$$

因此不能把第 1.2 节第二半的 1-一致性悄悄删掉。Rosser 的工作不是证明两种一致性本来等价，而是更换独立句，使普通一致性足够。

4.2 “真但不可证”不能省略相对系统与标准模型

附近的粗糙说法是：

“Gödel 证明了某些数学真理绝对不可证明。”

逐项修正：

1. $T⊬G_T$ 总是相对于指定理论 $T$；把 $G_T$ 加为新公理会得到证明它的更强理论。
2. “$G_T$ 为真”通常指 $\mathbb{N}\models G_T$，必须说明标准自然数模型与所选标准证明谓词。
3. 第一不完备定理首先是 syntactic independence（句法独立性）结果；它不把“所有可能的数学论证”压缩成一个绝对可证关系。
4. Rosser 句的优势是降低独立性假设，不是自动提供比 Gödel 句更透明的自然算术意义。

边界之所在是：provability（形式系统内可证性）、truth（给定结构中的真）与 acceptability（数学共同体接受的论证）属于不同关系，不能只用“证明”一词抹平。[1]

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

今日一问。 定义 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$ 在元意义下一致，那么对每个标准句子 $\sigma$，

$$T⊢\sigma ⟺\mathbb{N}\models {\mathrm{RProv}}_T(⌜\sigma ⌝).$$

既然它在标准模型中与普通可证性有相同外延，为什么不能直接用 ${\mathrm{RProv}}_T$ 取代 ${\mathrm{Prov}}_T$，照搬第二不完备定理？请分别审计下面两种内部原则是否仍可证明：

$$T⊢{\mathrm{RProv}}_T(⌜A\to B⌝)\to ({\mathrm{RProv}}_T(⌜A⌝)\to {\mathrm{RProv}}_T(⌜B⌝)),$$

以及

$$T⊢{\mathrm{RProv}}_T(⌜A⌝)\to {\mathrm{RProv}}_T(⌜{\mathrm{RProv}}_T(⌜A⌝)⌝).$$

方向提示。 不要只比较两谓词在 $\mathbb{N}$ 中选中了哪些句子；要追踪“把两份证明机械合成为一份证明”时，所得新编号是否仍赢得与相反证明的先后竞赛。外部 coextension（同延）不自动给出理论内部的可证等价。

数学地图。 本微弧的主线是

$$\text{Gödel 编码}⟶\text{对角引理}⟶\text{标准 Gödel 句}⟶\{\begin{array}{l}\text{一致性：不可证},\\ 1\text{-一致性：不可否证}\end{array}⟶\text{Rosser 有界证明竞赛}⟶\text{普通一致性下不完备}.$$

明日转向

$$\text{证明变换的算术化}⟶\text{可导条件}⟶\mathrm{Con}(T)⟶\text{第二不完备定理}⟶\text{Löb 定理与 provability logic}.$$

模型论邻支解释非标准证明见证；可计算性邻支把“完备且可枚举即可判定”的反证推进为 Church undecidability（Church 不可判定性）；证明论邻支则研究增加反射原则或超限归纳后，理论强度如何增长。

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

展开完整解答

模板：压缩迭代 + 几何尾和 (contraction iteration with geometric tail).

先把导数界转成整体压缩估计。任取 $x,y\in [0,1]$。若 $x=y$，结论显然；若 $x\ne y$，由中值定理，存在介于 $x,y$ 之间的 $\xi$ 使

$$\begin{array}{}\text{(3)}& |f(x)-f(y)|=|f^{\prime }(\xi )||x-y|\le q|x-y|.\end{array}$$

因为 $f([0,1])\subseteq [0,1]$，归纳可知每个 $x_n\in [0,1]$。对相邻迭代应用 $(3)$：

$$|x_{n+1}-x_n|=|f(x_n)-f(x_{n-1})|\le q|x_n-x_{n-1}|.$$

归纳得到，对每个 $n\ge 0$，

$$\begin{array}{}\text{(4)}& |x_{n+1}-x_n|\le q^n|x_1-x_0|.\end{array}$$

任取整数 $m>n\ge 0$，由三角不等式与 $(4)$，

$$\begin{array}{rl}|x_m-x_n|& \le \sum _{k=n}^{m-1}|x_{k+1}-x_k|\\ & \le |x_1-x_0|\sum _{k=n}^{m-1}{q}^k\\ & \le \frac{q^n}{1-q}|x_1-x_0|.\end{array}$$

因 $0\le q<1$，右端在 $n\to \mathrm{\infty }$ 时趋于 $0$，且该估计对所有 $m>n$ 一致。因此 $(x_n)$ 是 Cauchy 列。实数完备且 $[0,1]$ 闭，所以存在 $x_{\ast }\in [0,1]$ 使 $x_n\to x_{\ast }$。

由 $f$ 连续，

$$x_{\ast }=\underset{n\to \mathrm{\infty }}{lim}{x}_{n+1}=\underset{n\to \mathrm{\infty }}{lim}f(x_n)=f(x_{\ast }),$$

故 $x_{\ast }$ 是不动点。

令上面的 $m\to \mathrm{\infty }$，得到第一条误差界

$$|x_n-x_{\ast }|\le \frac{q^n}{1-q}|x_1-x_0|.$$

再直接把 $(3)$ 迭代到 $x_n$ 与不动点 $x_{\ast }$：

$$\begin{array}{rl}|x_n-x_{\ast }|& =|f(x_{n-1})-f(x_{\ast })|\\ & \le q|x_{n-1}-x_{\ast }|\\ & \le \cdots \le q^n|x_0-x_{\ast }|.\end{array}$$

最后证明唯一性。若 $y_{\ast }$ 也是不动点，则由 $(3)$，

$$|x_{\ast }-y_{\ast }|=|f(x_{\ast })-f(y_{\ast })|\le q|x_{\ast }-y_{\ast }|.$$

由于 $q<1$，只能有 $|x_{\ast }-y_{\ast }|=0$，即 $x_{\ast }=y_{\ast }$。

复用该模板时应保留五步：局部导数界变整体压缩；控制相邻增量；用几何尾和证明 Cauchy；用完备性与闭性保住极限；最后分别用连续性与压缩性证明不动点存在和唯一。

资料与来源 (Sources)

1. Stanford Encyclopedia of Philosophy, “Gödel’s Incompleteness Theorems,” 尤见 §§2.1、2.3–2.5 与 3.2：$\omega$-一致性／1-一致性、证明关系表示、Gödel 句两半证明、Rosser 改进及标准可证性谓词的可导条件。https://plato.stanford.edu/entries/goedel-incompleteness/
2. 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：原始 $\omega$-一致性框架、不可判定句构造与证明算术化。https://link.springer.com/article/10.1007/BF01700692
3. Barkley Rosser, “Extensions of some theorems of Gödel and Church,” Journal of Symbolic Logic 1(3), 87–91 (September 1936), DOI 10.2307/2269028：simple consistency 的定义、以普通一致性推出不可判定命题的改进；论文开篇 extract 已核验。https://doi.org/10.2307/2269028
4. David Hilbert, “Mathematical Problems,” lecture delivered at the International Congress of Mathematicians, Paris (1900), translated with the author’s permission by Mary Winston Newson, Bulletin of the American Mathematical Society 8(10), 437–479 (1902)：第二问题对算术公理相容性及有限逻辑推导的原始表述；第 3 节短引核自 AMS PDF。https://www.ams.org/journals/bull/1902-08-10/S0002-9904-1902-00923-3/S0002-9904-1902-00923-3.pdf