対角補題

数理論理学において、対角線の補題（対角化補題、自己言及補題^[1]、不動点定理 とも呼ばれる）は、自然数の特定の形式理論、特にすべての計算可能関数を表現できるほど強力な理論において自己言及 文が存在することを証明する。対角線の補題によって存在が保​​証された文は、ゲーデルの不完全性定理やタルスキの定義不可能性定理^[2]などの基本的な極限定理の結果を証明するために使用できる 。これは、集合論と数論における カントールの対角線論証 にちなんで名付けられている。

を自然数の集合とする。算術言語における一階の理論は、計算可能な関数を、言語における「グラフ」式が存在する場合、つまり、各に対してとなる式が存在する場合、表現する^{[3 ]。}${\displaystyle \mathbb {N} }$ ${\displaystyle T}$${\displaystyle f:\mathbb {N} \rightarrow \mathbb {N} }$ ${\displaystyle {\mathcal {G}}_{f}(x,y)}$${\displaystyle T}$${\displaystyle n\in \mathbb {N} }$

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

ここでは自然数 に対応する数値があり、これはにおける推定最初の数値の 番目の後続数として定義されます。 ${\displaystyle {}^{\circ }n}$${\displaystyle n}$${\displaystyle n}$${\displaystyle 0}$${\displaystyle T}$

対角補題では、すべての式に自然数（ とも表記）を体系的に割り当てることも求められます。自然数はゲーデル数と呼ばれます。式は、ゲーデル数に対応する数字で 内で表すことができます。たとえば、は次のように表されます。${\displaystyle {\mathcal {A}}}$${\displaystyle \#({\mathcal {A}})}$${\displaystyle \#_{\mathcal {A}}}$${\displaystyle T}$${\displaystyle {\mathcal {A}}}$${\displaystyle ^{\circ }\#_{\mathcal {A}}}$

対角線の補題は、すべての原始再帰関数を表現できる理論に適用されます。このような理論には、1 階のペアノ算術やより弱いロビンソン算術、さらには R として知られるはるかに弱い理論も含まれます。補題の一般的な記述 (以下に示す) では、理論がすべての計算可能な関数を表現できるというより強い仮定が立てられていますが、言及されているすべての理論にもその能力があります。

直感的に、は自己言及文です。 は、が特性 を持つと述べています。 この文は、与えられた文 の同値類に、文 の同値類を割り当てる操作の不動点と見ることもできます(文の同値類とは、理論 においてその文が同等であることが証明できるすべての文の集合です)。 証明で構築された文は、と文字通り同じではありませんが、理論 において同等であることが証明できます。 ${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {F}}}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {A}})}$${\displaystyle T}$${\displaystyle {\mathcal {C}}}$${\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$${\displaystyle T}$

次のように定義される関数があると します。${\displaystyle f:\mathbb {N} \to \mathbb {N} }$

${\displaystyle f(\#_{\mathcal {A}})=\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})]}$

理論上は自由変数が1つだけの各式 に対してとなり、そうでない場合は となります。ここで は式のゲーデル数 を表します。関数は計算可能（これはゲーデルの番号付けスキームに関する仮定です）なので、で を表す式が存在します。つまり、 ${\displaystyle {\mathcal {A}}(x)}$${\displaystyle x}$${\displaystyle T}$${\displaystyle f(n)=0}$${\displaystyle \#_{\mathcal {A}}=\#({\mathcal {A}}(x))}$${\displaystyle {\mathcal {A}}(x)}$${\displaystyle f}$${\displaystyle {\mathcal {G}}_{f}(x,\,y)}$${\displaystyle f}$${\displaystyle T}$

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

つまり

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

ここで、 1 つの自由変数を持つ任意の式が与えられた場合、式を次のように定義します。 ${\displaystyle {\mathcal {F}}(y)}$${\displaystyle y}$${\displaystyle {\mathcal {B}}(z)}$

${\displaystyle {\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]}$

次に、1 つの自由変数を持つすべての式について、次のようになります。 ${\displaystyle {\mathcal {A}}(x)}$

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

つまり

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

ここでを に置き換えて、文を次のように定義します。 ${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {B}}}$${\displaystyle {\mathcal {C}}}$

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

すると、前の行は次のように書き直すことができる。

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

これが望ましい結果です。

（[Raatikainen (2015a)]では、異なる言葉で同じ議論が述べられています。）

この補題はカントールの対角線論証に似ていることから「対角」と呼ばれている。^[5]「対角補題」や「不動点」という用語は、クルト・ゲーデルの1931年の論文やアルフレッド・タルスキの1936年の論文には登場しない。

ルドルフ・カルナップ(1934) は、一般自己言及的補題^[6]を初めて証明した。これは、ある条件を満たす理論Tの任意の式Fに対して、式ψが存在し、 ψ ↔ F (°#( ψ )) がTで証明可能であるというもの である。カルナップの研究は、計算可能関数の概念が1934 年にはまだ開発されていなかったため、別の言葉で表現された。メンデルソン(1997、p. 204) は、対角補題のようなものがゲーデルの推論に暗黙的に含まれていると述べたのはカルナップが初めてであると考えている。ゲーデルは 1937 年までにカルナップの研究を知っていた。^[7]

対角補題は計算可能性理論におけるクリーネの再帰定理と密接に関連しており、それぞれの証明は似ています。

• 間接的な自己言及
• 不動点定理の一覧
• 原始的な再帰演算
• 自己言及
• 自己言及的パラドックス

• ジョージ・ブーロスとリチャード・ジェフリー、1989年。計算可能性と論理、第3版。ケンブリッジ大学出版局。ISBN 0-521-38026 -X ISBN 0-521-38923-2   
• ルドルフ・カルナップ、1934年。 『言語の論理的統語論』。(英訳：2003年。『言語の論理的統語論』。オープンコート出版。)
• Haim Gaifman、2006年。「命名と対角化：カントールからゲーデル、そしてクリーネへ」。Logic Journal of the IGPL、14：709-728。
• ヒンマン、ピーター、2005年。数学論理の基礎。AKピーターズ。ISBN 1-56881-262-0 
• メンデルソン、エリオット、1997年。「数理論理学入門」、第4版。チャップマン＆ホール。
• パヌ・ラーティカイネン、2015a。対角化補題。スタンフォード哲学百科事典、編。ザルタ。 Raatikainen (2015b) の補足。
• Panu Raatikainen、2015b。ゲーデルの不完全性定理。スタンフォード哲学百科事典、Zalta 編。
• レイモンド・スマリヤン、1991年。 『ゲーデルの不完全性定理』オックスフォード大学出版局。
• レイモンド・スマリヤン、1994年。「対角化と自己言及」オックスフォード大学出版局。
• アルフレッド・タルスキー(1936)。 "Der Wahrheitsbegriff in den formalisierten Sprachen" (PDF)。ステューディア フィロソフィカ。1 : 261–405。2014年 1 月 9 日のオリジナル(PDF)からアーカイブ。2013 年6 月 26 日に取得。
  • アルフレッド・タルスキ、JH ウッドガー訳、1983 年。「形式化された言語における真理の概念」。タルスキの 1936 年論文の英訳。A. タルスキ編、J. コーコラン編、1983 年、『論理、意味論、メタ数学』、ハケット。