對角線引理

對角線引理（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]