3,094
个编辑
更改
跳到导航
跳到搜索
第422行：
第422行： + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
无编辑摘要
'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969">'''Lawvere, F. W. (1969).''' Diagonal arguments and cartesian closed categories. In ''Category Theory, Homology Theory and their Applications III'', Lecture Notes in Mathematics, vol. 92, Springer.【Lawvere 不动点定理，把 SRT、Gödel 不完备、Turing 停机统一为范畴论特例】【§5.6.2】</ref>。
'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969">'''Lawvere, F. W. (1969).''' Diagonal arguments and cartesian closed categories. In ''Category Theory, Homology Theory and their Applications III'', Lecture Notes in Mathematics, vol. 92, Springer.【Lawvere 不动点定理，把 SRT、Gödel 不完备、Turing 停机统一为范畴论特例】【§5.6.2】</ref>。
=== SRT与自指===
第二递归定理最直接、也最让人着迷的威力，是它'''一劳永逸地解释了"自指"现象为什么合法'''。但要先澄清一个容易混淆的关键点：这些里程碑可以从'''两个正交的维度'''来理解——
* '''结论的性质'''：是"否定性"（证否某物不存在：Cantor、Russell、Turing、Gödel），还是"肯定性"（证实自指对象存在：自复制、quine、SRT 本身）；
* '''结论活在哪个世界'''：纯集合论（SRT不适用），还是程序 / 可计算世界（可以用SRT）。
两个维度交叉，得到下表：
{| class="wikitable"
|-
!
! '''否定性结论'''（证否某物）
! '''肯定性结论'''（证实某物存在）
|-
| '''纯集合论'''（SRT不适用）
| [[康托尔论证实数不可数]]、[[罗素悖论]]
| （无）
|-
| '''程序 / 可计算'''（可以用SRT）
| '''[[图灵停机问题]]、[[哥德尔不完备定理]]'''
| [[冯诺伊曼自复制自动机]]、[[quine程序]]、[[自省程序]]、SRT 本身
|}
由此看清每个现象的双重身份：'''[[图灵停机问题]]、[[哥德尔不完备定理]]'''在"风格"上是否定性自指（与 [[康托尔不可数问题]]、[[罗素悖论]]同类），但它们活在程序世界，所以'''又能被 SRT 事后统一推出'''；康托尔不可数问题、罗素悖论位于纯集合论世界，SRT 造不出"实数"或"集合"，只能算'''同源但独立'''。下面逐个讲清楚。
==== 康托尔对角线论证（1891） ====
'''现象'''：实数集不可数。假设每个实数都被编号 <math>0, 1, 2, \ldots</math>；定义一个新实数，令它的第 <math>n</math> 位小数与"编号 <math>n</math> 的实数"的第 <math>n</math> 位小数都不同。这个新实数不在原表里——矛盾<ref name="cantor1891">'''Cantor, G. (1891).''' Über eine elementare Frage der Mannigfaltigkeitslehre. ''Jahresbericht der Deutschen Mathematiker-Vereinigung'', 1, 75–78.【对角线论证的源头】</ref>。
'''与 SRT 的关系：同源，但独立'''。两者做了同一件事——取"第 <math>i</math> 个对象在第 <math>i</math> 个位置上的值"（对角线）：康托尔取"第 <math>i</math> 个实数的第 <math>i</math> 位小数"，SRT 取"第 <math>e</math> 个程序在输入 <math>e</math> 上的值"<math>\phi_e(e)</math>（即证明里的 <math>S(e, e)</math>）。但'''方向相反'''：康托尔取对角线后'''改动'''它，制造一个"不在表里"的对象，从而证明实数'''不可数'''；SRT 取对角线后'''固定'''它，得到一个"引用自己编号"的程序，从而证明自指程序'''存在'''。注意，SRT '''推不出''' 康托尔定理——SRT 的结论都活在"程序 / 可计算"的世界里，给不出"实数不可数"这种纯集合论命题；两者只是共享了同一个技巧<ref name="cantor1891" /><ref name="moschovakis2010">'''Moschovakis, Y. N. (2010).''' Kleene's amazing second recursion theorem. ''The Bulletin of Symbolic Logic'', 16(2), 189–239.【18 个应用的权威综述；本文应用部分的章节编号均指此文】</ref>。