形式陈述

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

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

因此 $T$$T$ 不完备。证明把公式、证明和推导关系 Gödel 编码为自然数，利用对角引理构造能谈论自身可证性的句子；Rosser 改进用“较短的反证”比较把原证明所需的 $\omega$$\omega$-一致性降为普通一致性。

直觉

一旦一个有限可操作的系统足以描述自己的证明，它就能制造一个针对该证明机制的自指断言，使系统在保持一致时无法对其作出完整裁决。

例子与边界

Peano 算术与 ZFC 在一致的前提下都不能决定各自语言中的所有算术句子。定理不适用于所有数学理论：Presburger 算术较弱但完备且可判定；自然数结构的全部真句组成完备理论，却不是可有效公理化的。仅由一致性不能把任意独立句直接宣称为“标准模型中为真”；真值结论还需分析具体构造或更强的可靠性假设。

推论与应用

不完备性划定形式公理化、自动证明和元数学的基本边界，并引出第二不完备定理、可证明性逻辑及独立性研究。它否定的是“单个一致、有效、足够强的理论决定全部算术真值”，而不是数学证明或形式化本身。

参考资料

• 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。