對角線引理（），又稱為不動點定理（）。在數理邏輯中，對角線引理表明了自然數的形式理論中自指句子的存在——尤其是那些強到足以表示所有可計算函數的形式理論。
由對角線引理確立其存在的句子，將可用於證明一些邏輯的基礎限制，例如：哥德爾不完備定理或塔斯基不可定義定理。
背景
記自然數系為\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年注意到卡爾納普的工作。
注释
参考文献
评论 (0)