對角線引理

對角線引理（），又稱為不動點定理（）。在數理邏輯中，對角線引理表明了自然數的形式理論中自指句子的存在——尤其是那些強到足以表示所有可計算函數的形式理論。

由對角線引理確立其存在的句子，將可用於證明一些邏輯的基礎限制，例如：哥德爾不完備定理或塔斯基不可定義定理。See Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 ).

 背景 
記自然數系為。是一套帶有皮亞諾公理的一階邏輯理論。一个可計算函數可以在表達，若於中有合式公式使得：
 Hinman 2005, p. 316

此處的  是指對應於自然數  的數碼，也就是皮亞諾公理裡預先假定的第一數碼  的第個後繼

換句話說數碼是自然數的一種推廣，會依據第一數碼（常數符號）和後繼（函數符號）的語意解釋不同而有不同的實質意義。

對角線引理需要將內的每條合式公式 ，以有限運算步驟可以實現的方法，一對一的對應到一個自然數（簡寫為 ），這樣的就被稱為的哥德爾數（注意哥德爾數的指定方法不唯一）。如此一來，也可以用數碼來表示。

 引理的內容 
若 為一套帶有皮亞諾公理的一階邏輯理論，且所有可計算函數於能夠表達；而  內的合式公式  中的變數  是完全自由的。則有一條合式公式使得
Smullyan (1991, 1994) are standard specialized references. The lemma is Prop. 3.34 in Mendelson (1997), and is covered in many texts on basic mathematical logic, such as Boolos and Jeffrey (1989, sec. 15) and Hinman (2005).

 證明 
以下使用元語言敘述證明過程。讀者可以自己轉成以一階邏輯語言表達的正式證明。

對於  中有一完全自由變數  的合式公式 ，我們定義函數 為：

其他狀況下取  。顯然函數  是可計算的，故根據假設，存在合式公式 使得



然後對具有自由變數  的合式公式 ，定義  為：

注意到一階邏輯的公理模式（參見量词公理）



 是簡記  內所有自由的  被取代成項  所得到的新合式公式（而並非代表  只有一個組成變數）；而(A4)要成立，必須額外要求：若 是組成  的其中一個變數，則  內自由的  都不被  的量詞約束。（簡稱為項  對變數  於合式公式  是自由的）

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

所以從  的定義有



注意到從演绎定理會有




對定理(2)雙箭頭的後半部與公理模式(A4)使用MP律，然後套用(D')會有



而從等號的性質（奠基於皮亞諾公理），對所有的項  有

故(3)配合(D)會有



然後對等式和它的公理（同樣奠基於皮亞諾公理）施用兩次普遍化，然後與(A4)施用MP律兩次會有：

若項 和  都對變數  於自由，則


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



然後注意到另條量詞的公理模式（若  於合式公式  中完全不自由或不曾出現）


然後以普遍化於定理(4)外面補上 ，接著與(A5)一起套用MP律會有

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



總結(R-right)和(R-left)，然後帶入函數  的值有

注意  內變數  是完全自由的，故可以把前面推導中所有的  換成  ，然後定義

那我們可以從定理(5)得到

至此引理完成證明。

 歷史 

對角線引理跟可計算性理論中的Kleene's recursion theorem有密切的聯繫，證明方法也相似。

這個定理之所以被冠以「對角線」，是因為它與康托爾的對角論證法的形式很相近。「對角線引理」或「不動點」的詞彙並未出現在哥德爾1931年所發表的劃時代的論文中，也沒有出現在塔斯基1936年的論文中。卡爾納普是第一個人證明出：只要理論T滿足某些條件，那麼對於T中的任何式子ψ，都存在式子φ使得φ ↔ ψ(#(φ))在T中是可證的。由於在1934年尚未有可計算函數的概念，卡爾納普是以別的用詞去陳述該結論。Elliott Mendelson 認為是卡爾納普首先指出哥德爾的論證中隱含地運用了對角線引理，而哥德爾則是在1937年注意到卡爾納普的工作。See Gödel's Collected Works, Vol. 1, p. 363, fn 23.

 注释 

 参考文献 

Category:引理
Category:數理邏輯