更改

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

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

==== [[Lawvere 不动点定理]]（1969） ====

==== Lawvere不动点定理（笛卡尔闭范畴版本） ====

这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''[[范畴论]]统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的关系。

设 <math>\mathcal{(\mathcal{C})}</math> 为任意'''笛卡尔闭范畴'''（Cartesian closed category, CCC），<math>A</math> 和 <math>Y</math> 是 <math>\mathcal{C}</math> 中的任意对象。

'''[[Lawvere定理]]（标准陈述）'''：设 '''<math>C</math>''' 是一个 ''[[Cartesian 闭范畴]]''（Cartesian closed category，"对象 = 数据类型、[[态射]] = 数据类型间可计算变换、函数空间本身也是对象、可以反复变换"的信息世界）。设 '''<math>F: C \to C</math>''' 是一个[[函子]]（"世界内部的一种自我变换"）。如果存在一个'''满射态射'''（surjective morphism，形象地说"覆盖了 <math>F(A)</math> 的全部出口"）

则对象 <math>Y</math> 具有'''不动点性质'''：对任意自态射 <math>t : Y \to Y</math>，都存在点 <math>y : 1 \to Y</math>，满足:

:<math>y \cdot t = y</math>

: <math>f: A \to F(A)</math>     （每个 <math>F(A)</math> 元素都被 <math>f</math> 的像源元素覆写）

其逆否命题等价于：若 <math>Y</math> 上存在没有不动点的自态射，则不存在从 <math>A</math> 到 <math>Y^A</math> 的弱点满射。

那么对'''任意'''态射 <math>g: F(A)\to A</math>，都存在一个不动物 <math>x: A\to A</math>，使得

定理的核心洞察是：只要论域 <math>A</math> 足以编码所有从 <math>A</math> 到 <math>Y</math> 的函数，那么 <math>Y</math> 上的任何全局变换都无法避免不动点。这种结构是跨领域通用的：可计算性理论、数理逻辑、集合论中的所有经典对角线结果，都是这一抽象定理的具体实例。

: <math> F(x) \circ f = g \circ f</math>

===== 与SRT的对应 =====

{| class="wikitable"

 

'''直观解读'''：所谓"自指世界"，就是那种'''函数空间可以作为自身参数来研究'''的地方（Cartesian 闭）。在这种世界里，只要有一个"程序能撞出比自己更复杂的结果"的接口（[[满射]]态射），'''任何"全局选择函数"（<math>g</math>）都必有不动物'''——你的 <math>g</math> 想要把世界再次变换回自己，总会撞到某个无法再造新东西的点（<math>x</math>），而那个点正好让变换等于"再变换一次"（<math>F(x) = g</math>）。"自指 <math>\to </math>不动点"在这种世界里是不可避免的结构——不论那世界是自然数 + 可计算函数（Turing、Kleene），还是形式系统 + 可证性（Gödel），还是集合论宇宙（Russell、Cantor）。

 

{| class="wikitable"

| + Lawvere定理与克林第二递归定理的对应 |

|-

| --- |

! Lawvere 抽象成分

| ! Lawvere 抽象范畴概念 !! 克林第二递归定理中的具体对应 |

! SRT 实例化

| - |

|-

| 笛卡尔闭范畴 <math>\mathcal{(\mathcal{C})}</math> |

| Cartesian 闭范畴 <math>C</math>

| - |

| 取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi:\mathbb{N}^k\rightarrow\mathbb{N}</math> 的等价类"，[[态射]]是可计算变换；或者更技术地说，<math>P_\omega</math> 或 [[K1范畴]]（Gödel 编码的可计算函数论范畴）

| 对象 <math>A</math> |

|-

| - |

| [[函子]] <math>F</math>

| 对象 <math>Y</math> |

| 适当选取（<math>C</math> 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 <math>F</math> 取作"按编号 <math>e</math> 取 <math>\phi_e</math>" 的函子

| - |

|-

| 指数对象 <math>Y^A</math> |

| 满射态射 <math>f: A\to F(A)</math>

| - |

| 取定 [[#"可计算"与"部分函数"|§2.1]] 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 <math>e</math> 看作可枚举的元素、保证 <math>F(A)</math> 的每个元素都能表示为"以 <math>f(e)</math> 为参数的程序"，这一步在 SRT 证明中就是 [[#一行对角线|§5.2.1]] 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）

| 弱点满射 <math>g : A \to Y^A</math> |

|-

| - |

| 任意态射 <math>g: F(A)\to A</math>

| 自态射 <math>t : Y \to Y</math> |

| 取 <math>g =</math> SRT 推论里那个'''给定的全可计算函数 <math>f</math>'''（"按它编程序"）。注意：SRT 表述要求 <math>f:\mathbb{N} \to \mathbb{N}</math> 是'''全'''可计算的——Lawvere 框架对应"<math>f</math> 处处有定义"这一约束，保证 <math>g</math> 在 <math>F(A)</math> 的全部范围内都有意义。

| - |

|-

| 结论：<math>Y</math> 具有不动点性质 |

| 不动物 <math>x: A\to A</math>

| } |

| 正是 SRT 给出的那个'''不动点编号 <math>c</math>'''——它满足 <math>F(c) \circ f = g \circ f</math>，即 <math>\phi_c = \phi_{f(c)}</math>

|}

'''关系定性'''：

'''关系定性'''：