# 對角線引理

## 背景

${\displaystyle \vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {A}}_{f}(^{\circ }n,\,y)]}$ [2]

${\displaystyle {\begin{cases}^{\circ }1:=S(0_{T})\\^{\circ }(n+1):=S(^{\circ }n)\\\end{cases}}}$

## 引理的內容

${\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 f(\#_{{\mathcal {A}}(x)})=\#[{\mathcal {A}}(^{\circ }\#_{{\mathcal {A}}(x)})]}$

${\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {A}}_{f}(^{\circ }\#_{{\mathcal {A}}(x)},\,y)\Leftrightarrow [y=^{\circ }f(\#_{{\mathcal {A}}(x)})]\}}$  ${\displaystyle (1)}$

${\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 \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 })}$

${\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 \vdash _{T}S=S}$

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})\Rightarrow {\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]}$  ${\displaystyle (R-right)}$

${\displaystyle \vdash _{T}\,(S=U)\Rightarrow [{\mathcal {F}}(S)\Rightarrow {\mathcal {F}}(U)]}$  ${\displaystyle (E)}$

${\displaystyle \vdash _{T}\,{\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow \{[^{\circ }f(\#_{{\mathcal {A}}(x)})=y]\Rightarrow {\mathcal {F}}(y)\}}$  ${\displaystyle (4)}$

${\displaystyle (\forall y)({\mathcal {D}}\Rightarrow {\mathcal {E}})\Rightarrow [{\mathcal {D}}\Rightarrow (\forall y){\mathcal {E}}]}$  ${\displaystyle (A5)}$

${\displaystyle \vdash _{T}\,{\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow (\forall y)\{[^{\circ }f(\#_{{\mathcal {A}}(x)})=y]\Rightarrow {\mathcal {F}}(y)\}}$

${\displaystyle \vdash _{T}\,{\mathcal {F}}[^{\circ }f(\#_{{\mathcal {A}}(x)})]\Rightarrow {\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})}$  ${\displaystyle (R-left)}$

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{{\mathcal {A}}(x)})\Leftrightarrow {\mathcal {F}}\{^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{{\mathcal {A}}(x)})]\}}$  ${\displaystyle (5)}$

${\displaystyle {\mathcal {C}}:={\mathcal {B}}(^{\circ }\#_{{\mathcal {B}}(x)})}$

${\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$

## 注释

1. ^ 如果把自然數單純視為計算符號數量的記號，那這邊"函數"的意義單純代表的是這種記號的一對一對應。並非一定要理解成以公理化集合論有序對為基礎定義的函數

## 参考文献

1. ^ See Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 ).
2. ^ 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.