対角線補題

数理論理学において、対角線補題（対角化補題、自己参照補題、または不動点定理 とも呼ばれる）は、特定の形式理論における自己参照文の存在を証明する。

対角補題の特定の例は、 1931 年にクルト・ゲーデルが不完全性定理の証明を構築するために使用し、また 1933 年にタルスキが定義不可能性定理を証明するために使用しました。1934 年にカルナップが、ある程度の一般性で対角補題を初めて発表しました。^{[ 1 ]}対角補題は、集合論と数論におけるカントールの対角論法にちなんで名付けられました。

対角補題は、対角関数を表現できる十分強力な理論であればどれでも適用できます。そのような理論には、1 階ペアノ算術が含まれます。${\displaystyle {\mathsf {PA}}}$より弱いロビンソン算術${\displaystyle {\mathsf {Q}}}$理論も同様に${\displaystyle {\mathsf {Q}}}$（つまり、それを解釈する）。^{[ 2 ]}補題の一般的な記述（以下に示す）では、理論がすべての（全体の）計算可能な関数を表現できるというより強い仮定を置いているが、言及されているすべての理論もその能力を持っている。

対角補題：${\displaystyle T}$一次理論である${\displaystyle {\mathsf {Q}}}$（ロビンソン算術）そして${\displaystyle \psi (x)}$言語の任意の式である${\displaystyle T}$わずか${\displaystyle x}$自由変数として。次に文があります${\displaystyle \varphi }$言語で${\displaystyle T}$そのため${\displaystyle T\vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )}$。

直感的に、${\displaystyle \varphi }$は、自己言及的な文であり、「${\displaystyle \psi }$。

証明:${\displaystyle diag_{T}:\mathbb {N} \to \mathbb {N} }$各式のコードを関連付ける計算可能な関数とする${\displaystyle \varphi (x)}$自由変数が1つだけ${\displaystyle x}$言語で${\displaystyle T}$閉じた式のコードとともに${\displaystyle \varphi (\ulcorner \varphi \urcorner )}$（つまり、${\displaystyle \ulcorner \varphi \urcorner }$の中へ${\displaystyle \varphi }$のために${\displaystyle x}$） そして${\displaystyle 0}$他の議論のために。（事実、${\displaystyle diag_{T}}$計算可能かどうかは、ゲーデル数の選択に依存する（ここでは標準的な数を用いる）。

表現定理により、${\displaystyle T}$は、計算可能なすべての関数を表します。したがって、式が存在します。${\displaystyle \delta (x,y)}$代表${\displaystyle diag_{T}}$特に、それぞれについて${\displaystyle \varphi (x)}$、${\displaystyle T\vdash \delta (\ulcorner \varphi \urcorner ,y)\leftrightarrow y=\ulcorner \varphi (\ulcorner \varphi \urcorner )\urcorner }$。

させて${\displaystyle \psi (x)}$任意の式のみ${\displaystyle x}$自由変数として定義します。${\displaystyle \chi (x)}$として${\displaystyle \exists y(\delta (x,y)\land \psi (y))}$、そして${\displaystyle \varphi }$なれ${\displaystyle \chi (\ulcorner \chi \urcorner )}$すると、次の同値関係が証明できる。${\displaystyle T}$:

${\displaystyle \varphi \leftrightarrow \chi (\ulcorner \chi \urcorner )\leftrightarrow \exists y(\delta (\ulcorner \chi \urcorner ,y)\land \psi (y))\leftrightarrow \exists y(y=\ulcorner \chi (\ulcorner \chi \urcorner )\urcorner \land \psi (y))\leftrightarrow \exists y(y=\ulcorner \varphi \urcorner \land \psi (y))\leftrightarrow \psi (\ulcorner \varphi \urcorner )}$。

対角線補題には様々な一般化が存在する。ここではそのうちのいくつかのみを紹介する。特に、以下の最初の3つの一般化の組み合わせによって新たな一般化が得られる。^{[ 4 ]}${\displaystyle T}$一次理論である${\displaystyle {\mathsf {Q}}}$（ロビンソン算術）

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

1934年、ルドルフ・カルナップは、任意の式に対して、ある一定の一般性をもって対角線補題を初めて発表した。${\displaystyle \psi (x)}$と${\displaystyle x}$自由変数として（十分に表現力のある言語において）、文が存在する${\displaystyle \varphi }$そのため${\displaystyle \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )}$（ある標準モデルでは）真である。^{[ 7 ]}カルナップの研究は、証明可能性ではなく真理の観点から表現された（つまり、構文的ではなく意味論的に）。^{[ 8 ]}さらに、計算可能な関数の概念は1934年にはまだ開発されていなかった。

対角補題は計算可能性理論におけるクリーネの再帰定理と密接に関連しており、それぞれの証明は類似している。^{[ 9 ]} 1952年、レオン・ヘンキンは、自身の証明可能性を述べる文は証明可能かどうかを問いかけた。彼の問いは、特にレーブの定理と証明可能性論理を用いた対角補題のより一般的な分析につながった。^{[ 10 ]}

• 間接的な自己言及
• 不動点定理一覧
• 自己参照
• 自己言及的なパラドックス

• ジョージ・ブーロス、リチャード・ジェフリー、1989年。『計算可能性と論理学』第3版。ケンブリッジ大学出版局。ISBN 0-521-38026-XISBN 0-521-38923-2
• ルドルフ・カルナップ、1934年。『言語の論理構文論』（英語訳：2003年、オープン・コート出版）。
• Haim Gaifman、2006年。「命名と対角線化：カントールからゲーデル、クリーネへ」。IGPLの論理学ジャーナル、14: 709–728。

• Robert G. Jeroslow、1973年。「ゲーデルの第2不完全性定理に対するヒルベルト＝ベルネイスの導出可能性条件における冗長性」。『記号論理学ジャーナル』、38.3: 359–367。

• ペトル・ハジェク＆パベル・プドラーク、2016年（初版1998年）。一階算術のメタ数学。スプリンガー・フェルラーグ。

• ピーター・ヒンマン、2005年。『数理論理学の基礎』 AKピーターズ。ISBN 1-56881-262-0
• メンデルソン、エリオット、1997年。『数理論理学入門』第4版、チャップマン＆ホール。
• パヌ・ラーティカイネン、2015a。対角化補題。スタンフォード哲学百科事典、編。ザルタ。
• Panu Raatikainen、2015b。「ゲーデルの不完全性定理」。『スタンフォード哲学百科事典』、Zalta 編。
• レイモンド・スムリアン、1991年。『ゲーデルの不完全性定理』オックスフォード大学出版局。
• レイモンド・スムリアン、1994年。『対角線化と自己参照』オックスフォード大学出版局。
• Craig Smoryński、2023年。「形式的対角化の初期の歴史」。Logic Journal of the IGPL、31.6: 1203–1224。
• アルフレッド・タルスキー(1936)。"Der Wahrheitsbegriff in den formalisierten Sprachen" (PDF)。ステューディア フィロソフィカ。1 : 261–405。2014年 1 月 9 日のオリジナル(PDF)からアーカイブ。2013 年6 月 26 日に取得。
• アルフレッド・タルスキ、JH・ウッドガー訳、1983年。「形式言語における真理の概念」。タルスキの1936年の論文の英訳。A・タルスキ、J・コーコラン編、1983年、『論理、意味論、メタ数学』、ハケット社。