哥德尔第一不完备定理

形式陈述

设 $T$ 是可有效公理化的一阶理论，语言足以表达基本算术，并至少包含 Robinson 算术 $Q$ 的能力。Gödel–Rosser 形式的第一不完备定理断言：若 $T$ 一致，则存在 Rosser 句 $R_T$ ，使

T\nvdash R_T, \qquad T\nvdash\neg R_T.

因此 $T$ 不完备。证明把公式、证明和推导关系 Gödel 编码为自然数，再利用对角引理构造能谈论证明机制的句子。原始 Gödel 句 $G_T$ 近似断言“ $G_T$ 在 $T$ 中不可证明”，为排除 $T\vdash\neg G_T$ 需要比普通一致性更强的 $\omega$ -一致性或相应可靠性假设；Rosser 句改为比较一句话及其否定的最短证明，把定理前提降为普通一致性。

直觉

可有效编码的语法让理论间接谈论自己的证明。原始 Gödel 构造把对角化压进一句近似“我在本理论中不可证明”的 $G_T$ ：若理论证明它，便与一致性冲突；要让否定也不可证，还需原始版本的更强假设。Rosser 改进不再只靠这句朴素自述，而让候选句比较正反两类证明的先后，从而仅凭一致性仍迫使系统无法裁决。这个机制要求理论足以表示基本算术，并不波及所有形式系统。

例子与边界

Peano 算术与 ZFC 都属于适用范围：若它们一致，就不能决定各自语言中的所有算术句子。Presburger 算术较弱却完备且可判定，纯命题逻辑也有完备的可判定证明系统，因为二者都不具备编码上述证明机制所需的算术表达力。另一侧，自然数结构的全部真句组成完备理论，却不是可有效公理化的。仅凭一致性也不能把任意独立句宣称为“标准模型中为真”；真值结论仍取决于具体构造或更强的可靠性假设。

推论与应用

形式系统的证明可被 Gödel 编码，对角思想据此产生自指句。第一不完备定理由此划定 Peano 算术等理论的句法极限，并通向第二不完备定理、可证明性逻辑、不可判定性与独立性研究。它否定的是“单个一致、有效、足够强的理论决定全部算术真值”，而不是数学证明或形式化本身。

参考资料

Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§3.4, incompleteness and arithmetization of syntax。
Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Chs. VII–VIII, Gödel and Rosser incompleteness theorems。

形式陈述 ​

反向链接

形式陈述