对角线引理

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

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

## 背景

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

$\vdash_{T}\,(\forall y)[(^\circ f(n)=y) \Leftrightarrow \mathcal{A}_f(^\circ n,\,y)]$

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

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

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

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

## 引理的内容

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

$\vdash_T\,\mathcal{C}\Leftrightarrow\mathcal{F}({}^{\circ}\#_{\mathcal{C}})$

## 证明

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

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

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

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

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

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

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

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

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

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

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

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

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

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

注意到从演绎定理会有

$\mathcal{D}_1\Rightarrow(\mathcal{D}_2\Rightarrow\mathcal{D}_3),\,\mathcal{D}_2\vdash_T\,\mathcal{D}_1\Rightarrow\mathcal{D}_3$ $(D)$

$\mathcal{D}_1\Rightarrow\mathcal{D}_2,\,\mathcal{D}_2\Rightarrow\mathcal{D}_3\vdash_T\,\mathcal{D}_1\Rightarrow\mathcal{D}_3$ $(D^{\prime})$

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

$\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)})]\}$ $(3)$

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

$$\vdash_{T} S=S$$

故(3)配合(D)会有

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$$\vdash_T\,\mathcal{C}\Leftrightarrow\mathcal{F}(^{\circ}\#_{\mathcal{C}})$$

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

## 历史

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

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