更改

'''与"一行证明"的关系'''：§5.3 的证明把表上 <math>D^* = E_m</math> 的循环直接写成 <math>\psi(S(e,e), x)</math> 的柯里化形式——<math>h(x) = \phi_x(x)</math> 对应"<math>e </math>= 编号(<math>\psi(S(y,y), x)</math>)"，<math>S(e,e)</math> 就是用自应用把表上的对角线点亮；'''列表法只是把这一行在表格里完整地展开'''。两者本质相同：列表法暴露了"为什么沿对角线循环必会撞回表里"——'''每行 <math>E_k</math> 都被对角线穿一格，循环天然闭合'''。

'''与"一行证明"的关系'''：§5.3 的证明把表上 <math>D^* = E_m</math> 的循环直接写成 <math>\psi(S(e,e), x)</math> 的柯里化形式——<math>h(x) = \phi_x(x)</math> 对应"<math>e </math>= 编号(<math>\psi(S(y,y), x)</math>)"，<math>S(e,e)</math> 就是用自应用把表上的对角线点亮；'''列表法只是把这一行在表格里完整地展开'''。两者本质相同：列表法暴露了"为什么沿对角线循环必会撞回表里"——'''每行 <math>E_k</math> 都被对角线穿一格，循环天然闭合'''。

 

[[文件:列表法证明.png|缩略图|'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 E_0, E_1, E_2, E_k，每格填 \phi_{\phi_i(j)}；主对角线（红圈）上的格子构成对角枚举 D。'''黄底 D 行'''：把对角线上的格子抽出，得到 D = (\phi_{\phi_0(0)}, \phi_{\phi_1(1)}, \phi_{\phi_2(2)}, \ldots)。'''D* 行'''：把 f 套到 D 上得到 D* = (\phi_{f(\phi_0(0))}, \phi_{f(\phi_1(1))}, \ldots)——可计算 \Rightarrow 必是某行 E_m。'''绿框'''：取 k = m 撞上 E_m，得 \phi_{\phi_m(m)} = \phi_{f(\phi_m(m))}，再设 n = \phi_m(m) 即得 \phi_n = \phi_{f(n)}——f 的不动点。]]


'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0</math>, <math>E_1</math>, <math>E_2</math>, <math>E_k</math>，每格填 <math>\phi_\phi_i(j)</math>；主对角线（红圈）上的格子构成对角枚举 <math>D</math>。'''黄底 <math>D</math> 行'''：把对角线上的格子抽出，得到 <math>D = (\phi_\phi_0(0),\phi_\phi_1(1),\phi_\phi_2(2), \ldots)</math>。*''<math>D</math>'' 行*''：把 <math>f</math> 套到 <math>D</math> 上得到 <math>D'' = (\phi_{f(\phi_0(0))},\phi_{f(\phi_1(1))},\ldots</math>)——可计算 <math>\Rightarrow </math>必是某行 <math>E_m</math>。'''绿框'''：取 <math>k = m</math> 撞上 <math>E_m</math>，得 <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>，再设 <math>n = \phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——<math>f</math> 的不动点。

'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0</math>, <math>E_1</math>, <math>E_2</math>, <math>E_k</math>，每格填 <math>\phi_\phi_i(j)</math>；主对角线（红圈）上的格子构成对角枚举 <math>D</math>。'''黄底 <math>D</math> 行'''：把对角线上的格子抽出，得到 <math>D = (\phi_\phi_0(0),\phi_\phi_1(1),\phi_\phi_2(2), \ldots)</math>。*''<math>D</math>'' 行*''：把 <math>f</math> 套到 <math>D</math> 上得到 <math>D'' = (\phi_{f(\phi_0(0))},\phi_{f(\phi_1(1))},\ldots</math>)——可计算 <math>\Rightarrow </math>必是某行 <math>E_m</math>。'''绿框'''：取 <math>k = m</math> 撞上 <math>E_m</math>，得 <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>，再设 <math>n = \phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——<math>f</math> 的不动点。