對角線引理

對角線引理（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年注意到卡爾納普的工作。