哥德尔第一不完备定理

形式陈述

设 $T$ 是有效语言中的经典一阶理论，其公理集递归可枚举，并且 $T$ 扩张 Robinson 算术 $Q$ 。Gödel–Rosser 第一不完备定理断言：若 $T$ 一致，则存在算术句子 $R$ ，使

T\nvdash R,\qquad T\nvdash\neg R.

这里的一致性只要求不存在同时可证的句子及其否定，不要求所有定理在标准自然数中都真，也不要求 $\omega$ -一致性。下面构造 $R$ ，并分别完成两方向的反证。

这里把公理按有效编码看作有限字语言；“递归可枚举”是可识别性，不是仅说集合可数。Robinson 算术 $Q$ 使用语言 $\{0,S,+,\times\}$ ，其七条公理是下面各式的全称闭包：

\begin{gathered} Sx\ne0,\qquad Sx=Sy\to x=y,\qquad x\ne0\to\exists y\,x=Sy,\\ x+0=x,\qquad x+Sy=S(x+y),\\ x\times0=0,\qquad x\times Sy=(x\times y)+x. \end{gathered}

它不含归纳模式。以下固定数码的有限推导使用这些公理，但不会把它们误当成一般归纳。

固定语法与证明编码。外部关系 $\mathrm{Proof}_T(p,a)$ 表示“自然数 $p$ 编码一份结论代码为 $a$ 的 $T$ 证明”。若公理只能枚举，就在每个公理行附上它被枚举出来的阶段证书；核验只需模拟指定的有限步。这使带证书的证明关系原始递归，且不改变可证句集合。它不要求公理成员关系本身可判定。

取 $Q$ 中双向数码可表示的公式 $P(p,a)$ 和 $N(p,a)$ ，分别表示上述证明关系，以及“ $p$ 是代码为 $a$ 的句子的否定的证明”。对每对标准数，关系成立时 $Q$ 证明对应公式，不成立时 $Q$ 证明其否定。原始递归关系在 $Q$ 中的这一表示定理是本证明的基础接口；算术可表示性页详细证明了 PA 版本， $Q$ 版本见参考资料，不把 PA 内的归纳直接搬进 $Q$ 。

记 $\overline n=S^n0$ ，并在 $Q$ 中约定

x\le y\;:\equiv\;\exists z(z+x=y).

对公式

A(a):=\forall p\bigl(P(p,a)\to \exists q(q\le p\land N(q,a))\bigr)

使用 $Q$ 版本的对角引理，得到 $R$ 。令 $r=\operatorname{code}(R)$ ，则

Q\vdash R\leftrightarrow \forall p\bigl(P(p,\overline r)\to \exists q(q\le p\land N(q,\overline r))\bigr).\tag{R}

$N$ 已经包含否定编码操作，因此它的第二个参数仍是 $\overline r$ 。这避免把元语言中的编码函数当成新算术函数符号。

直觉

原始 Gödel 句近似表达“我没有证明”。一致性足以排除它可证；排除其否定则还需更强条件。Rosser 句改用一种可有限核验的比较：“每份正方证明，都有编号不更大的反方证明。”编号是编码后的自然数，不必等于证明长度，也不表示证明质量。

假如找到正方证明 $m$ ，只需排除 $0,\ldots,m$ 这些反方候选，便能在理论内否定 Rosser 条件。假如找到反方证明 $n$ ，则把任意正方候选分成两部分：有限的小编号逐个排除，其余编号已经可以用 $n$ 作反方见证。两个方向都只把有限多份外部核验结果合并成内部证明。

例子与边界

固定数码的两个有限引理

$Q$ 没有归纳公理，但它有后继非零、后继单射、每个非零数有前驱，以及 $z+0=z$ 、 $z+Sx=S(z+x)$ 。对每个外部固定的 $n\in\mathbb N$ ，这些公理给出两份有限证明：

Q\vdash\forall x\left(x\le\overline n\to \bigvee_{k=0}^{n}x=\overline k\right),\tag{F_n}

Q\vdash\forall x\left( \bigvee_{k=0}^{n-1}x=\overline k\ \lor\ \overline n\le x\right).\tag{C_n}

$n=0$ 时第二式的有限析取为空，剩下 $0\le x$ ，其见证是 $z=x$ 。

证明的方法是把前驱公理重复有限次。重复 $n$ 次给出

x=\overline0\lor\cdots\lor x=\overline{n-1} \lor\exists w\,x=S^n w.

最后一支中，加法公理展开 $n$ 次得到 $w+\overline n=S^n w=x$ ，所以 $\overline n\le x$ ；这证明 $(C_n)$ 。这里 $S^n w$ 是元语言对含 $n$ 个后继的有限项的缩写。

为证明 $(F_n)$ ，把前驱公理展开 $n+1$ 次。若不在 $0,\ldots,n$ 的数码分支，就有 $x=S^{n+1}w$ 。假设 $x\le\overline n$ ，取见证 $z$ ，则

\overline n=z+S^{n+1}w=S^{n+1}(z+w).

反复使用后继单射，最后得到一个后继等于 $0$ ，矛盾。因此尾部分支被排除， $(F_n)$ 成立。这个推导没有使用加法交换律或 $Q$ 中的一般归纳。

例如，对固定的 $3$ ， $(F_3)$ 将 $x\le\overline3$ 化成四个等号分支； $(C_3)$ 将任意 $x$ 分成 $x=\overline0,\overline1,\overline2$ 与 $\overline3\le x$ 。所以若已有四份 $Q\vdash\theta(\overline k)$ （ $k=0,1,2,3$ ），等号替换和有限析取消去给出

Q\vdash\forall x(x\le\overline3\to\theta(x)).

这里是在元理论中为每个 $n$ 制造有限证明，没有把数码 $\overline n$ 换成变量，再声称 $Q$ 已证明一个统一的线性序定理。

第一方向： $T$ 不能证明 $R$

反设 $T\vdash R$ ，取一份真实证明的标准编号 $m$ 。数码表示给出

Q\vdash P(\overline m,\overline r).

由外部一致性，不存在任何真实的 $\neg R$ 证明。因此，对有限的 $k=0,\ldots,m$ ，逐一有

Q\vdash\neg N(\overline k,\overline r).

使用 $(F_m)$ ，把这些定理合并为

Q\vdash\forall q(q\le\overline m\to \neg N(q,\overline r)).

另一方面，在 $T$ 中由假定的定理 $R$ 和式 (R)，代入 $p=\overline m$ ，可推出

T\vdash\exists q(q\le\overline m\land N(q,\overline r)).

这与上一条 $Q$ 定理（因而也是 $T$ 定理）矛盾。故 $T\nvdash R$ 。没有从“ $T$ 证明存在反方证明”直接跳到“真有反方证明”；冲突完全发生在 $T$ 的形式推导中。

第二方向： $T$ 不能证明 $\neg R$

反设 $T\vdash\neg R$ ，取一份真实证明的标准编号 $n$ 。于是

Q\vdash N(\overline n,\overline r).

一致性排除真实的 $R$ 证明。只取其中有限的 $k=0,\ldots,n-1$ ，便有 $Q\vdash\neg P(\overline k,\overline r)$ 。现在在 $Q$ 内取任意 $p$ ，用 $(C_n)$ 分情况：

若 $p=\overline k$ ，其中 $k<n$ ，则 $\neg P(p,\overline r)$ ，所以式 (R) 中的条件式成立。
若 $\overline n\le p$ ，以 $q=\overline n$ 为存在见证。由已经证明的 $N(\overline n,\overline r)$ ，得 $\exists q(q\le p\land N(q,\overline r))$ ，条件式仍成立。

解除分情况并全称概括，得到 $Q$ 证明式 (R) 的右端，因而 $Q\vdash R$ ，也就有 $T\vdash R$ 。这与反设的 $T\vdash\neg R$ 违反一致性，故 $T\nvdash\neg R$ 。若 $n=0$ ，第一部分为空，第二部分覆盖所有候选，论证照样成立。

这个方向没有把“每个标准 $k$ 都不是正方证明”升级成 $Q\vdash\forall p\neg P(p,\overline r)$ ；实际使用的只有小于固定 $n$ 的有限清单。

假设的适用边界

PA 是 $Q$ 的扩张，因而若 PA 一致，上述结论直接适用。ZFC 通过其可有效形式化的自然数算术解释得到同类结论；它属于解释版本，而非与 $Q$ 使用相同原始语言的字面扩张。

Presburger 算术只有加法及相应语言中的归纳，变量乘法不可定义，其有效公理系统可以完备且可判定。纯命题逻辑也有完备的可判定证明系统；它们不满足这里的算术表达条件。另一侧，自然数结构的全部算术真句组成完备理论，却不是有效可公理化的。

本构造的 $R$ 在一致性假设下还确实为真：没有真实的 $R$ 证明，所以式 (R) 的每个标准实例前件都假； $Q$ 的固定点等价在标准模型中成立。这是对这个具体构造的语义分析，不能据此宣称任意独立句都真，也未额外断言所写公式已有某种最简算术层级形式。

推论与应用

对形式系统，若一致、有效公理化且每个句子均可决定，就能同时枚举 $\varphi$ 与 $\neg\varphi$ 的证明，等先出现的一边，从而判定所有句子。不完备性说明，包含上述算术机制的理论不能同时满足这些条件。

给 $T$ 加入一个独立句可以决定该句，但只要新理论仍一致、有效且扩张 $Q$ ，就会产生相对于新证明系统的新 Rosser 句。一阶完备性并未失效：它断言在理论所有模型中都成立的句子可证；这里的结论意味着同一个一致算术理论有模型对某些句子给出不同真值。

第二不完备定理提出的是另一个特定目标：在标准证明谓词满足可导出条件时，理论不能证明自己的标准一致性句。这里的 Rosser 定理只承诺存在双向不可证句，并不把任意写成“我一致”的公式都自动纳入结论；两者的证明谓词与内部推导条件须分别核对。

验收练习。 分别从假设的证明编号 $m$ 与 $n$ 出发，列出实际需要核验的有限集合，标出 $(F_m)$ 与 $(C_n)$ 的用途，并指出外部一致性在哪一步排除了真实证明。若答案中出现从无限多份数码证明直接推出无界全称定理，就还没有完成 Rosser 的有限比较。

参考资料

Peter Smith，An Introduction to Gödel’s Theorems，corrected second edition，§10.3，§§11.3、11.8，§17，§§25.3、26.1：固定数码序引理见印刷72–73、81–82页， $Q$ 的原始递归表示见124–128页，Rosser 的 $\le$ 版本见188–189页，有效公理化扩展见191–192页。本文用前驱公理的有限展开直接证明所需两个引理。
Open Logic Project，The Open Logic Text: Incompleteness，rev. 9620cc7，§3.7、§5.4，Lemmas 3.24–3.25、Theorem 5.7：固定数码比较与 Rosser 双向证明；该书使用严格小于的版本，本文始终使用不大于。

形式陈述 ​

固定数码的两个有限引理 ​

第一方向：T 不能证明 R ​

第二方向：T 不能证明 ¬R ​

假设的适用边界 ​

反向链接

形式陈述

固定数码的两个有限引理

第一方向： $T$ 不能证明 $R$

第二方向： $T$ 不能证明 $\neg R$

假设的适用边界