| 第414行: |
第414行: |
| | '''关系定性''': | | '''关系定性''': |
| | | | |
| − | - [[#Lawvere 不动点定理(1969)|Lawvere 不动点定理]]'''不是''' SRT 的"推论"(该定理没有反推 SRT,而是反过来把 SRT 概括出来);
| + | * [[#Lawvere 不动点定理(1969)|Lawvere 不动点定理]]'''不是''' SRT 的"推论"(该定理没有反推 SRT,而是反过来把 SRT 概括出来); |
| − | - Lawvere 也不仅是 SRT 的"更高层次表述"(它是数学基础层面的定理,把 SRT、[[#Gödel 不动点引理(对角引理)|Gödel 不动点引理]]、Turing 停机问题的不可判定性、Russell 悖论、Cantor 对角线'''全部统一为这一个抽象结构的不同时面''');
| + | * Lawvere 也不仅是 SRT 的"更高层次表述"(它是数学基础层面的定理,把 SRT、[[#Gödel 不动点引理(对角引理)|Gödel 不动点引理]]、Turing 停机问题的不可判定性、Russell 悖论、Cantor 对角线'''全部统一为这一个抽象结构的不同侧面'''); |
| − | - 因此在写作时应避免两种过度描述:①"Lawvere 推翻了 SRT 的独立性"(错,它们不在一个抽象层);②"SRT 是 Lawvere 的特例,所以 SRT 的定理就是 Lawvere 给出来的"(错,Lawvere 是更高层的解释,不是 SRT 证明的工具;SRT 证明仍然是 §5.3 的[[对角线论证]])。
| + | * 因此应避免两种过度描述:①"Lawvere 推翻了 SRT 的独立性"(错,它们不在一个抽象层);②"SRT 是 Lawvere 的特例,所以 SRT 的定理就是 Lawvere 给出来的"(错,Lawvere 是更高层的解释,不是 SRT 证明的工具;SRT 证明仍然是 §5.3 的[[对角线论证]])。 |
| | | | |
| − | '''对读者的现实意义''':如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域,理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算,§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969" />。 | + | '''对读者的现实意义''':如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域,理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算,§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969" />。 |
| | | | |
| | === 自指现象:SRT 的"自指"一面 === | | === 自指现象:SRT 的"自指"一面 === |