對角線引理

维基百科,自由的百科全书
跳转至: 导航搜索

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

由對角線引理確立其存在的句子,將可用於證明一些邏輯的基礎限制,例如:哥德爾不完備定理塔斯基不可定義定理[1]

背景[编辑]

自然數集N。稱一個理論能表示所有可計算函數f : NN,若於T中存在某式子δ(x,y),使得對任意nT可以證明:

(∀y) [f(n) = y ↔ δ(n,y)].[2]

此處的 n 是指對應於自然數n的數碼,其定義為閉項 1+ ··· +1 (n個1),而f(n)是對應於f(n)的數碼。

對角線引理也要求有一種系統化方式,去給每個式子θ指派一個自然數#(θ),其中#(θ)稱為θ的哥德爾數。然后,任何的式子便可在理論T中,以對應於其自身的哥德爾數的數碼所表示。

對角線引理可以應用到那些足以表示所有原始遞歸函數的理論。此類理論包括皮亞諾算術,以及較弱的鲁宾逊算术英语Robinson arithmetic。該引理的一個較普遍的陳述是(如下一小節所示),作較強的假定,即是假設理論T可以表示所有可計算函數。

引理的內容[编辑]

令T為算術語言的一階理論,且它能夠表示所有可計算函數。令ψ為該語言中具有單一自由變量的一個式子。

對角線引理告訴我們:存在一個式子φ,使得φ↔ψ(#(φ))這式子在T裡是可證明的。[3]

直覺上,φ是一個表示「φ具有性質ψ」的自指句子。句子φ可被視為將每個式子θ映射到句子ψ(#(θ))的運算的不動點。這個證明構造出的句子φ並非字面上與ψ(#(φ))相同,但在理論T中它們是可證等價的。

證明[编辑]

定義函數f: NN為:

f(#(θ)) = #(θ(#(θ)))

對於任何含有單一自由變量的 T-公式 θ 成立。否則,便設 f(n) = 0。函數 f 是可計算的,所以 T 中存在能代表 f 的式子 δ。所以對于任何式子 θ,T 可以證明

(∀y) [ δ(#(θ),y) ⇔ y = f(#(θ))],

換言之

(∀y) [ δ(#(θ),y) ⇔ y = #(θ(#(θ)))].

現定義式子 β(z) 為:

β(z) = (∀y) [δ(z,y) ⇒ ψ(y)],

那麼

β(#(θ)) ⇔ (∀y) [ y = #(θ(#(θ))) ⇒ ψ(y)],

也就是說

β(#(θ)) ⇔ ψ(#(θ(#(θ))))

設 φ 為句子 β(#(β))。然后我們可於 T 中證明:

(*) φ ⇔ (∀y) [ δ(#(β),y) ⇒ ψ(y)] ⇔ (∀y) [ (y = #(β(#(β))) ⇒ ψ(y)].


T 的框架下,分析以下兩種情況:
1. 假設 φ 成立,在(*)最右的部分中把 #(β(#(β)) 代入到 y,便得到:

(#(β(#(β)) = #(β(#(β))) → ψ(#(β(#(β))),

由於 φ 即 β(#(β)),故此 ψ(#(φ)) 成立。
2. 另一方面,假設 ψ(#(β(#(β)))) 成立。那麼(*)最右的部分必然成立,所以 φ 也為真。

綜上,φ ↔ ψ(#(φ)) 在 T 中是可證的。證明完畢。

歷史[编辑]

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

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

參考資料[编辑]

  1. ^ See Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 ).
  2. ^ For details on representability, see Hinman 2005, p. 316
  3. ^ 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).
  4. ^ See Gödel's Collected Works, Vol. 1, p. 363, fn 23.