Gödel 第二不完备定理

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

第二不完备定理把第一定理的自指机制内部化：一个足够强且一致的可有效理论不能在自身内部证明标准形式化的一致性陈述 $\mathrm{Con}(T)$。它并非说理论的一致性无法在任何更强系统中证明，而是说系统不能用自身认可的证明机制完成这一任务。对“一致性”如何算术化以及理论满足哪些可导出条件，陈述必须精确。

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

对每个固定的有限证明长度 $N$，PA 可以逐一检查“长度不超过 $N$ 的字符串都不是 $0=1$ 的 PA 证明”这一有限断言；这并不等于 PA 证明统一的

后者量化所有可能长度。若 PA 一致，第二不完备定理排除这种内部统一证明。更强理论可以证明较弱理论的一致性，而不一致理论反而能证明任何句子，所以一致性与可导出条件都是不可删的假设。

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

第一不完备定理公理库哥德尔第一不完备定理Gödel's first incompleteness theorem足够强、有效公理化且一致的算术理论存在既不可证也不可否证的句子。提供不可判定句，Hilbert–Bernays 可导出条件让证明谓词在理论内运作。结果限制 Hilbert 纲领式的内部一致性证明，并推动相对一致性、序数分析公理库序数Ordinal由属于关系良序且具有传递性的集合，表征良序的同构类型。与更强元理论的研究。