数理論理学では、対角化定理（対角線補題（diagonal lemma）、対角化補題（diagonalization lemma）、自己言及補題（self-reference lemma）または不動点定理（fixed point theorem）としても知られる）は、自然数の特定の形式理論、特にすべての計算可能関数を表すのに十分な強力な理論における、自己言及的の存在を示す定理である。対角化定理によって存在が保証される文は、ゲーデルの不完全性定理やタルスキの定義不可能性定理といった基礎的な限界の証明に利用できるBoolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 )を参照のこと。。
背景 を自然数の集合とする。算術の言語における一階 と計算可能関数について、「がを表現（represent）表現可能性の詳細については、Hinman 2005, p. 316を参照のことする」とは、各に対して以下が成り立つ「グラフ」論理式がの言語に存在することをいう。
ここで、は自然数に対応する数詞（numeral）であり、における最初の数詞の番目の後者（successor）と定義される（）。
対角化定理はまた、すべての式に対して、そのゲーデル数と呼ばれる自然数（とも表記される）を割り当てる体系的な方法を必要とする。すると、式は内でそのゲーデル数に対応する数詞によって表せる。例えば、はによって表せる。
対角化定理は、原始再帰関数を全て表現できるような理論に対して適用される。そのような理論には、一階ペアノ算術や、より弱いロビンソン算術、さらにはRとして知られるはるかに弱い理論も含まれる。定理の一般的なステートメント（後述）は、理論が全ての計算可能関数を表現できるというより強い仮定を立てるが、前述の各理論はその能力を持っている。
定理のステートメント
直感的には、は自己言及的文である。は、が性質を持つことを述べている。また、文は、与えられた文の同値類に対して、文の同値類を割り当てる操作の不動点と見なすこともできる。証明の中で構成された文は、と字面上は同じではないが、理論において論理的に同値である。
証明 を、理論における1つの自由変数のみを持つ各論理式に対して以下のように定義された関数とする。
ただし、は式のゲーデル数を表す。また、以外のに対してはとする。この関数は計算可能である(これは根源的にはゲーデル数の割り当て方法（Gödel numbering scheme）に関する仮定である)ので、においてを表現する式が存在する。すなわち
つまり
ここで、1つの自由変数を持つ任意の式が与えられたとき、式を以下のように定義する。
すると、1つの自由変数を持つ全ての式に対して以下が成り立つ。
つまり
ここで、をに置き換え、文を以下のように定義する。
すると、前の行は以下のように書き直すことができる。
これが求める結果である。
(異なる用語による同じ議論は、Raatikainen (2015a)で与えられている。)
歴史 対角化定理はカントールの対角線論法と類似しているため、「対角化」と呼ばれる例えば、Gaifman (2006)を参照のこと。。「対角化定理」または「不動点」という用語は、クルト・ゲーデルのやアルフレト・タルスキの1936年の論文には登場しない。
ルドルフ・カルナップ (1934)は、一般自己言及補題（general self-reference lemma）を最初に証明したKurt Gödel, Collected Works, Volume I: Publications 1929–1936, Oxford University Press, 1986, p. 339.。これは、特定の条件を満たす理論における任意の式に対して、がで証明可能であるような式が存在することを述べている。カルナップの研究は異なる用語で表現されていた。なぜなら、計算可能関数の概念は1934年にはまだ開発されていなかったからである。（1997, p. 204）は、対角化定理のようなものがゲーデルの推論に暗黙的に含まれていると述べたのはカルナップが最初であると信じている。ゲーデルは1937年までにはカルナップの研究を知っていたゲーデルのCollected Works, Vol. 1, Oxford University Press, 1986, p. 363, fn 23を参照のこと。。
対角化定理は、計算可能性理論におけるクリーネの再帰定理と密接に関連しており、それぞれの証明は類似している。
関連項目
不動点定理の一覧 原始帰納的算術 自己言及 自己言及のパラドックス
脚注 出典
注釈
参考文献 George Boolos and Richard Jeffrey, 1989. Computability and Logic, 3rd ed. Cambridge University Press. Rudolf Carnap, 1934. Logische Syntax der Sprache. (English translation: 2003. The Logical Syntax of Language. Open Court Publishing.) Haim Gaifman, 2006. 'Naming and Diagonalization: From Cantor to Gödel to Kleene'. Logic Journal of the IGPL, 14: 709–728. Hinman, Peter, 2005. Fundamentals of Mathematical Logic. A K Peters. Mendelson, Elliott, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall. Panu Raatikainen, 2015a. The Diagonalization Lemma. In Stanford Encyclopedia of Philosophy, ed. Zalta. Supplement to Raatikainen (2015b). Panu Raatikainen, 2015b. Gödel's Incompleteness Theorems. In Stanford Encyclopedia of Philosophy, ed. Zalta. Raymond Smullyan, 1991. Gödel's Incompleteness Theorems. Oxford Univ. Press. Raymond Smullyan, 1994. Diagonalization and Self-Reference. Oxford Univ. Press.
Alfred Tarski, tr. J. H. Woodger, 1983. "The Concept of Truth in Formalized Languages". English translation of Tarski's 1936 article. In A. Tarski, ed. J. Corcoran, 1983, Logic, Semantics, Metamathematics, Hackett.