更改

==== Gödel 不动点引理（对角引理） ====

==== Gödel 不动点引理（对角引理） ====

对任何包含足够算术的递归可公理化理论 T，对 T 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 T 证 <math>\psi</math> ↔ <math>\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（一致性、<math>\omega</math>-一致性、不[[可判定性]]三层）见 §5.7.4 的详述。

对任何包含足够算术的递归可公理化理论 <math>T</math>，对 <math>T</math> 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 <math>T</math> 可证 <math>\psi\iff\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（一致性、<math>\omega</math>-一致性、不[[可判定性]]三层）见 §5.7.4 的详述。

注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。

注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。