查看“︁對角線引理”︁的源代码

'''對角線引理'''（{{lang|en|diagonal lemma}}），又稱為'''不動點定理'''（{{lang|en|fixed point theorem}}）。在[[數理邏輯]]中，對角線引理表明了自然數的[[形式系統|形式理論]]中[[自指]][[句子 (數理邏輯)|句子]]的存在——尤其是那些強到足以表示所有[[可計算函數]]的形式理論。

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

== 背景 ==
記[[自然數|自然數系]]為<math>\mathbb{N}</math>。<math>T</math>是一套帶有[[皮亞諾公理]]的一階邏輯理論。一个[[可計算函數]]<math>f: \mathbb{N}\rightarrow\mathbb{N}</math>{{NoteTag|如果把自然數單純視為計算符號數量的記號，那這邊"函數"的意義單純代表的是這種記號的一對一對應。並非一定要理解成以[[公理化集合論]]的[[有序對]]為基礎定義的[[函數]]。}}可以在<math>T</math>'''表達'''，若於<math>T</math>中有[[合式公式]]<math>\mathcal{A}_f(x, y)</math>使得：
: <math>\vdash_{T}\,(\forall y)[(^\circ f(n)=y) \Leftrightarrow \mathcal{A}_f(^\circ n,\,y)]</math><ref>Hinman 2005, p.&nbsp;316</ref>

此處的 <math>^\circ n</math> 是指對應於自然數 <math>n</math> 的'''數碼'''，也就是皮亞諾公理裡預先假定的第一數碼 <math>0_T</math> 的第<math>n</math>個後繼

:<math>
\begin{cases}
^\circ 1:= S(0_T)\\
^\circ (n+1):=S(^\circ n)\\
\end{cases}
</math>

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

對角線引理需要將<math>T</math>內的每條合式公式<math>\mathcal{A}</math> ，'''以有限運算步驟可以實現的方法'''，一對一的對應到一個自然數<math>\#(\mathcal{A})</math>（簡寫為 <math>\#_{\mathcal{A}}</math>），這樣的<math>\#_{\mathcal{A}}</math>就被稱為<math>\mathcal{A}</math>的[[哥德爾數]]（注意哥德爾數的指定方法不唯一）。如此一來，<math>\mathcal{A}</math>也可以用數碼<math>^{\circ}\#_{\mathcal{A}}</math>來表示。

== 引理的內容 ==
若<math>T</math> 為一套帶有[[皮亞諾公理]]的[[一階邏輯]]理論，且所有可計算函數於<math>T</math>能夠表達；而 <math>T</math> 內的合式公式 <math>\mathcal{F}(y)</math> 中的變數 <math>y</math> 是完全[[自由變量和約束變量|自由]]的。則有一條合式公式<math>\mathcal{C}</math>使得
:<math>\vdash_T\,\mathcal{C}\Leftrightarrow\mathcal{F}({}^{\circ}\#_{\mathcal{C}})</math><ref>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).</ref>

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

對於 <math>T</math> 中有一完全自由變數 <math>x</math> 的合式公式 <math>\mathcal{A}(x)</math>，我們定義函數<math>f:\mathbb{N}\to\mathbb{N}</math> 為：

:<math>f(\#_{\mathcal{A}(x)}) = \#[\mathcal{A}(^{\circ}\#_{\mathcal{A}(x)})]</math>

其他狀況下取 <math>f(n)=0</math> 。顯然函數 <math>f</math> 是可計算的，故根據假設，存在合式公式 <math>\mathcal{A}_f(x,\,y)</math>使得

:<math>\vdash_T\,(\forall y)\{\mathcal{A}_f(^{\circ}\#_{\mathcal{A}(x)},\,y) \Leftrightarrow [y = ^{\circ}f(\#_{\mathcal{A}(x)})]\}</math> <math>(1)</math>

然後對具有自由變數 <math>y</math> 的合式公式 <math>\mathcal{F}(y)</math>，定義 <math>\mathcal{B}(x)</math> 為：

:<math>\mathcal{B}(x) := (\forall y) [\mathcal{A}_f(x,\,y)\Rightarrow \mathcal{F}(y)]</math>

注意到一階邏輯的[[公理模式]]（參見[[一阶逻辑#量词公理|量词公理]]）

:<math>(\forall y)\mathcal{D}(y)\Rightarrow\mathcal{D}(S)</math> <math>(A4)</math>

:<math>\mathcal{D}(S)</math> 是簡記 <math>\mathcal{D}(y)</math> 內所有自由的 <math>y</math> 被取代成[[一阶逻辑#項|項]] <math>S</math> 所得到的新合式公式（而'''並非'''代表 <math>\mathcal{D}(y)</math> 只有一個組成變數）；而(A4)要成立，必須額外要求：若<math>s_i</math> 是組成 <math>S</math> 的其中一個變數，則 <math>\mathcal{D}(y)</math> 內自由的 <math>y</math> 都不被 <math>s_i</math> 的量詞約束。（簡稱為項 <math>S</math> 對變數 <math>y</math> 於合式公式 <math>\mathcal{D}(y)</math> 是自由的）

(A4)配合(1)使用[[肯定前件|MP律]]有

:<math>\vdash_T\,[\mathcal{A}_f(^{\circ}\#_{\mathcal{A}(x)},\,y)] \Leftrightarrow [y = ^{\circ}f(\#_{\mathcal{A}(x)})]</math>

所以從 <math>\mathcal{B}(x)</math> 的定義有

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

注意到從[[演绎定理]]會有

:<math>\mathcal{D}_1\Rightarrow(\mathcal{D}_2\Rightarrow\mathcal{D}_3),\,\mathcal{D}_2\vdash_T\,\mathcal{D}_1\Rightarrow\mathcal{D}_3</math> <math>(D)</math>
:<math>\mathcal{D}_1\Rightarrow\mathcal{D}_2,\,\mathcal{D}_2\Rightarrow\mathcal{D}_3\vdash_T\,\mathcal{D}_1\Rightarrow\mathcal{D}_3</math> <math>(D^{\prime})</math>

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

:<math>\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)})]\}</math> <math>(3)</math>

而從等號的性質（奠基於[[皮亞諾公理]]），對所有的項 <math>S</math> 有

:<math>\vdash_{T} S=S</math>

故(3)配合(D)會有

:<math>\vdash_T\,\mathcal{B}(^{\circ}\#_{\mathcal{A}(x)}) \Rightarrow \mathcal{F}[^{\circ}f(\#_{\mathcal{A}(x)})]</math> <math>(R-right)</math> 

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

:若項<math>S</math> 和 <math>U</math> 都對變數 <math>y</math> 於<math>\mathcal{F}(y)</math>自由，則
:<math>\vdash_{T}\,(S=U)\Rightarrow[\mathcal{F}(S)\Rightarrow\mathcal{F}(U)]</math> <math>(E)</math>

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

:<math>\vdash_{T}\,\mathcal{F}[^{\circ}f(\#_{\mathcal{A}(x)})]\Rightarrow\{[^{\circ}f(\#_{\mathcal{A}(x)})=y]\Rightarrow\mathcal{F}(y)\}</math> <math>(4)</math>

然後注意到另條量詞的公理模式（若 <math>y</math> 於合式公式 <math>\mathcal{D}</math> 中完全不自由或不曾出現）
:<math>(\forall y)(\mathcal{D}\Rightarrow\mathcal{E})\Rightarrow[\mathcal{D}\Rightarrow(\forall y)\mathcal{E}]</math> <math>(A5)</math>

然後以[[普遍化]]於定理(4)外面補上 <math>\forall y</math>，接著與(A5)一起套用MP律會有

:<math>\vdash_{T}\,\mathcal{F}[^{\circ}f(\#_{\mathcal{A}(x)})]\Rightarrow(\forall y)\{[^{\circ}f(\#_{\mathcal{A}(x)})=y]\Rightarrow\mathcal{F}(y)\}</math>

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

:<math>\vdash_T\,\mathcal{F}[^{\circ}f(\#_{\mathcal{A}(x)})] \Rightarrow \mathcal{B}(^{\circ}\#_{\mathcal{A}(x)})</math> <math>(R-left)</math>

總結(R-right)和(R-left)，然後帶入函數 <math>f</math> 的值有
:<math>\vdash_T\,\mathcal{B}(^{\circ}\#_{\mathcal{A}(x)}) \Leftrightarrow \mathcal{F}\{^{\circ}\#[\mathcal{A}(^{\circ}\#_{\mathcal{A}(x)})]\}</math> <math>(5)</math>
注意 <math>\mathcal{B}(x)</math> 內變數 <math>x</math> 是完全自由的，故可以把前面推導中所有的 <math>\mathcal{A}</math> 換成 <math>\mathcal{B}</math> ，然後定義
:<math>\mathcal{C}:= \mathcal{B}(^{\circ}\#_{\mathcal{B}(x)})</math>
那我們可以從定理(5)得到
:<math>\vdash_T\,\mathcal{C}\Leftrightarrow\mathcal{F}(^{\circ}\#_{\mathcal{C}})</math>
至此引理完成證明。<math>\Box</math>

== 歷史 ==

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

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

== 注释 ==
{{NoteFoot}}

== 参考文献 ==
{{Reflist}}

[[Category:引理]]
[[Category:數理邏輯]]