对角线引理

对角线引理（diagonal lemma），又称为不动点定理（fixed point theorem）。在数理逻辑中，对角线引理表明了自然数的形式理论中自指句子的存在——尤其是那些强到足以表示所有可计算函数的形式理论。

由对角线引理确立其存在的句子，将可用于证明一些逻辑的基础限制，例如：哥德尔不完备定理或塔斯基不可定义定理。^[1]

背景

记自然数系为${\displaystyle \mathbb {N} }$。${\displaystyle T}$是一套带有皮亚诺公理的一阶逻辑理论。一个可计算函数${\displaystyle f:\mathbb {N} \rightarrow \mathbb {N} }$^{[注 1]}可以在${\displaystyle T}$表达，若于${\displaystyle T}$中有合式公式${\displaystyle {\mathcal {A}}_{f}(x,y)}$使得：

${\displaystyle \vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {A}}_{f}(^{\circ }n,\,y)]}$^[2]

此处的 ${\displaystyle ^{\circ }n}$ 是指对应于自然数 ${\displaystyle n}$ 的数码，也就是皮亚诺公理里预先假定的第一数码 ${\displaystyle 0_{T}}$ 的第${\displaystyle n}$个后继

${\displaystyle {\begin{cases}^{\circ }1:=S(0_{T})\\^{\circ }(n+1):=S(^{\circ }n)\\\end{cases}}}$

换句话说数码是自然数的一种推广，会依据第一数码（常数符号）和后继（函数符号）的语意解释不同而有不同的实质意义。

对角线引理需要将${\displaystyle T}$内的每条合式公式${\displaystyle {\mathcal {A}}}$ ，以有限运算步骤可以实现的方法，一对一的对应到一个自然数${\displaystyle \#({\mathcal {A}})}$（简写为 ${\displaystyle \#_{\mathcal {A}}}$），这样的${\displaystyle \#_{\mathcal {A}}}$就被称为${\displaystyle {\mathcal {A}}}$的哥德尔数（注意哥德尔数的指定方法不唯一）。如此一来，${\displaystyle {\mathcal {A}}}$也可以用数码${\displaystyle ^{\circ }\#_{\mathcal {A}}}$来表示。

引理的内容

若${\displaystyle T}$ 为一套带有皮亚诺公理的一阶逻辑理论，且所有可计算函数于${\displaystyle T}$能够表达；而 ${\displaystyle T}$ 内的合式公式 ${\displaystyle {\mathcal {F}}(y)}$ 中的变数 ${\displaystyle y}$ 是完全自由的。则有一条合式公式${\displaystyle {\mathcal {C}}}$使得

${\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}({}^{\circ }\#_{\mathcal {C}})}$^[3]

证明

以下使用元语言叙述证明过程。读者可以自己转成以一阶逻辑语言表达的正式证明。

对于 ${\displaystyle T}$ 中有一完全自由变数 ${\displaystyle x}$ 的合式公式 ${\displaystyle {\mathcal {A}}(x)}$，我们定义函数${\displaystyle f:\mathbb {N} \to \mathbb {N} }$ 为：

${\displaystyle f(\#_{{\mathcal {A}}(x)})=\#[{\mathcal {A}}(^{\circ }\#_{{\mathcal {A}}(x)})]}$

其他状况下取 ${\displaystyle f(n)=0}$ 。显然函数 ${\displaystyle f}$ 是可计算的，故根据假设，存在合式公式 ${\displaystyle {\mathcal {A}}_{f}(x,\,y)}$使得

${\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {A}}_{f}(^{\circ }\#_{{\mathcal {A}}(x)},\,y)\Leftrightarrow [y=^{\circ }f(\#_{{\mathcal {A}}(x)})]\}}$ ${\displaystyle (1)}$

然后对具有自由变数 ${\displaystyle y}$ 的合式公式 ${\displaystyle {\mathcal {F}}(y)}$，定义 ${\displaystyle {\mathcal {B}}(x)}$ 为：

${\displaystyle {\mathcal {B}}(x):=(\forall y)[{\mathcal {A}}_{f}(x,\,y)\Rightarrow {\mathcal {F}}(y)]}$

注意到一阶逻辑的公理模式（参见量词公理）

${\displaystyle (\forall y){\mathcal {D}}(y)\Rightarrow {\mathcal {D}}(S)}$ ${\displaystyle (A4)}$

${\displaystyle {\mathcal {D}}(S)}$ 是简记 ${\displaystyle {\mathcal {D}}(y)}$ 内所有自由的 ${\displaystyle y}$ 被取代成项 ${\displaystyle S}$ 所得到的新合式公式（而并非代表 ${\displaystyle {\mathcal {D}}(y)}$ 只有一个组成变数）；而(A4)要成立，必须额外要求：若${\displaystyle s_{i}}$ 是组成 ${\displaystyle S}$ 的其中一个变数，则 ${\displaystyle {\mathcal {D}}(y)}$ 内自由的 ${\displaystyle y}$ 都不被 ${\displaystyle s_{i}}$ 的量词约束。（简称为项 ${\displaystyle S}$ 对变数 ${\displaystyle y}$ 于合式公式 ${\displaystyle {\mathcal {D}}(y)}$ 是自由的）

(A4)配合(1)使用MP律有

${\displaystyle \vdash _{T}\,[{\mathcal {A}}_{f}(^{\circ }\#_{{\mathcal {A}}(x)},\,y)]\Leftrightarrow [y=^{\circ }f(\#_{{\mathcal {A}}(x)})]}$

所以从 ${\displaystyle {\mathcal {B}}(x)}$ 的定义有

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})\Leftrightarrow (\forall y)\{[y=^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow {\mathcal {F}}(y)\}}$ ${\displaystyle (2)}$

注意到从演绎定理会有

${\displaystyle {\mathcal {D}}_{1}\Rightarrow ({\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}),\,{\mathcal {D}}_{2}\vdash _{T}\,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}}$ ${\displaystyle (D)}$

${\displaystyle {\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{2},\,{\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}\vdash _{T}\,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}}$ ${\displaystyle (D^{\prime })}$

对定理(2)双箭头的后半部与公理模式(A4)使用MP律，然后套用(D')会有

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})\Rightarrow \{[^{\circ }f(\#_{{\mathcal {A}}(x)})=^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow {\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\}}$ ${\displaystyle (3)}$

而从等号的性质（奠基于皮亚诺公理），对所有的项 ${\displaystyle S}$ 有

${\displaystyle \vdash _{T}S=S}$

故(3)配合(D)会有

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})\Rightarrow {\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]}$ ${\displaystyle (R-right)}$

然后对等式和它的公理（同样奠基于皮亚诺公理）施用两次普遍化，然后与(A4)施用MP律两次会有：

若项${\displaystyle S}$ 和 ${\displaystyle U}$ 都对变数 ${\displaystyle y}$ 于${\displaystyle {\mathcal {F}}(y)}$自由，则

${\displaystyle \vdash _{T}\,(S=U)\Rightarrow [{\mathcal {F}}(S)\Rightarrow {\mathcal {F}}(U)]}$ ${\displaystyle (E)}$

所以从(D)和演绎定理有

${\displaystyle \vdash _{T}\,{\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow \{[^{\circ }f(\#_{{\mathcal {A}}(x)})=y]\Rightarrow {\mathcal {F}}(y)\}}$ ${\displaystyle (4)}$

然后注意到另条量词的公理模式（若 ${\displaystyle y}$ 于合式公式 ${\displaystyle {\mathcal {D}}}$ 中完全不自由或不曾出现）

${\displaystyle (\forall y)({\mathcal {D}}\Rightarrow {\mathcal {E}})\Rightarrow [{\mathcal {D}}\Rightarrow (\forall y){\mathcal {E}}]}$ ${\displaystyle (A5)}$

然后以普遍化于定理(4)外面补上 ${\displaystyle \forall y}$，接著与(A5)一起套用MP律会有

${\displaystyle \vdash _{T}\,{\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow (\forall y)\{[^{\circ }f(\#_{{\mathcal {A}}(x)})=y]\Rightarrow {\mathcal {F}}(y)\}}$

所以上面的定理和定理(2)配合(D')有

${\displaystyle \vdash _{T}\,{\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow {\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})}$ ${\displaystyle (R-left)}$

总结(R-right)和(R-left)，然后带入函数 ${\displaystyle f}$ 的值有

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})\Leftrightarrow {\mathcal {F}}\{^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{{\mathcal {A}}(x)})]\}}$ ${\displaystyle (5)}$

注意 ${\displaystyle {\mathcal {B}}(x)}$ 内变数 ${\displaystyle x}$ 是完全自由的，故可以把前面推导中所有的 ${\displaystyle {\mathcal {A}}}$ 换成 ${\displaystyle {\mathcal {B}}}$ ，然后定义

${\displaystyle {\mathcal {C}}:={\mathcal {B}}(^{\circ }\#_{{\mathcal {B}}(x)})}$

那我们可以从定理(5)得到

${\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$

至此引理完成证明。${\displaystyle \Box }$

历史

对角线引理跟可计算性理论中的Kleene's recursion theorem有密切的联系，证明方法也相似。

这个定理之所以被冠以“对角线”，是因为它与康托尔的对角论证法的形式很相近。“对角线引理”或“不动点”的词汇并未出现在哥德尔1931年所发表的划时代的论文中，也没有出现在塔斯基1936年的论文中。卡尔纳普是第一个人证明出：只要理论T满足某些条件，那么对于T中的任何式子ψ，都存在式子φ使得φ ↔ ψ(#(φ))在T中是可证的。由于在1934年尚未有可计算函数的概念，卡尔纳普是以别的用词去陈述该结论。Elliott Mendelson 认为是卡尔纳普首先指出哥德尔的论证中隐含地运用了对角线引理，而哥德尔则是在1937年注意到卡尔纳普的工作。^[4]