更改

* 因此应避免两种过度描述：①"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">'''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 停机统一为范畴论特例】【§[[#Lawvere 不动点定理（1969）|5.6.2]]】</ref>。

=== SRT与自指===

=== SRT与自指===