形式陈述

设 $T$$T$ 是一致、递归可公理化并含有足够初等算术的理论，例如 PA 的一致递归可公理化扩张。对标准证明谓词 $\operatorname{Pr}_T(x)$${\mathrm{Pr}}_T(x)$，在 $T$$T$ 内把一致性形式化为

$$ \operatorname{Con}(T)\equiv\neg\operatorname{Pr}_T(\ulcorner 0=1\urcorner). $$$$\mathrm{Con}(T)\equiv \mathrm{\neg }{\mathrm{Pr}}_T(⌜0=1⌝).$$

Gödel 第二不完备定理断言 $T\nvdash\operatorname{Con}(T)$$T⊬\mathrm{Con}(T)$。证明利用可证明性条件和对角化，把第一不完备现象内化为关于“本理论不存在矛盾证明”的算术句子。结论依赖所选的标准可证明性谓词与足够强度；它不是对任意弱系统或任意自称“一致”的公式都成立的无条件口号。

直觉

一个能编码自身证明的足够强理论，无法只凭自己的规则给出完全可信的“我永不推出矛盾”证书；任何内部证书仍属于待评价的同一证明系统。

例子与边界

若 PA 一致，则 PA 不能证明 $\operatorname{Con}(\mathrm{PA})$$\mathrm{Con}(\mathrm{PA})$；更强的理论如 ZFC 可以在适当形式化下证明 PA 的一致性，而 Gödel 定理随后限制 ZFC 证明自身一致性。定理不说数学家不能给出相对一致性证明，也不说 $\operatorname{Con}(T)$$\mathrm{Con}(T)$ 在标准自然数中为假。若 $T$$T$ 不一致，它反而能证明所有句子，包括自己的“一致性”；所以一致性假设不可删。对极弱理论、非递归公理集或人为扭曲的可证明性谓词，结论需要另行分析。第一不完备定理给出不可判定句，第二定理专门限制内部一致性证明，二者不能互相替代。

推论与应用

该定理界定形式化自验证的边界，推动相对一致性、证明论序数和可信计算基的研究，也解释为何强系统的可靠性通常要在外部或更强元理论中论证。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，Ch. 3, arithmetization and the second incompleteness theorem。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Ch. 3, derivability conditions and consistency statements。