この項目では、数理論理学における概念について説明しています。名前の元になった証明テクニックについては「カントールの対角線論法 」を、行列の対角行列への変形については「対角化 」をご覧ください。
数理論理学 では、対角化定理 [ 注釈 1] [ 1] 自然数 の特定の形式理論、特にすべての計算可能関数 を表すのに十分な強力な理論における、自己言及 的文 （英語版 ） ゲーデルの不完全性定理 やタルスキの定義不可能性定理 などの基本的な限界を証明するために使用できる[ 2]
N
{\displaystyle \mathbb {N} }
自然数 の集合とする。算術の言語における一階 理論 （英語版 ）
T
{\displaystyle T}
f
:
N
→
N
{\displaystyle f:\mathbb {N} \rightarrow \mathbb {N} }
T
{\displaystyle T}
論理式
G
f
(
x
,
y
)
{\displaystyle {\mathcal {G}}_{f}(x,y)}
n
∈
N
{\displaystyle n\in \mathbb {N} }
f
{\displaystyle f}
表現 （represent）[ 3]
⊢
T
(
∀
y
)
[
(
∘
f
(
n
)
=
y
)
⇔
G
f
(
∘
n
,
y
)
]
{\displaystyle \vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {G}}_{f}(^{\circ }n,\,y)]}
ここで、
∘
n
{\displaystyle {}^{\circ }n}
n
{\displaystyle n}
数詞 （numeral）であり、
T
{\displaystyle T}
0
{\displaystyle 0}
n
{\displaystyle n}
対角化定理はまた、すべての式
A
{\displaystyle {\mathcal {A}}}
ゲーデル数 と呼ばれる自然数
#
(
A
)
{\displaystyle \#({\mathcal {A}})}
#
A
{\displaystyle \#_{\mathcal {A}}}
T
{\displaystyle T}
A
{\displaystyle {\mathcal {A}}}
∘
#
A
{\displaystyle ^{\circ }\#_{\mathcal {A}}}
対角化定理は、原始再帰関数 を全て表せる理論に適用される。そのような理論には、一階ペアノ算術 や、より弱いロビンソン算術 、さらにはRとして知られるはるかに弱い理論も含まれる。定理の一般的なステートメント（後述）は、理論が全ての計算可能関数 を表せるというより強い仮定を立てるが、前述の各理論はその能力を持っている。
直感的には、
C
{\displaystyle {\mathcal {C}}}
自己言及 的文である。
C
{\displaystyle {\mathcal {C}}}
C
{\displaystyle {\mathcal {C}}}
F
{\displaystyle {\mathcal {F}}}
C
{\displaystyle {\mathcal {C}}}
A
{\displaystyle {\mathcal {A}}}
F
(
∘
#
A
)
{\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {A}})}
不動点 と見なすこともできる[ 注釈 2]
T
{\displaystyle T}
C
{\displaystyle {\mathcal {C}}}
F
(
∘
#
C
)
{\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}
T
{\displaystyle T}
f
:
N
→
N
{\displaystyle f:\mathbb {N} \to \mathbb {N} }
T
{\displaystyle T}
x
{\displaystyle x}
A
(
x
)
{\displaystyle {\mathcal {A}}(x)}
f
(
#
A
)
=
#
[
A
(
∘
#
A
)
]
{\displaystyle f(\#_{\mathcal {A}})=\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})]}
ただし、
#
A
=
#
(
A
(
x
)
)
{\displaystyle \#_{\mathcal {A}}=\#({\mathcal {A}}(x))}
A
(
x
)
{\displaystyle {\mathcal {A}}(x)}
#
A
{\displaystyle \#_{\mathcal {A}}}
n
{\displaystyle n}
f
(
n
)
=
0
{\displaystyle f(n)=0}
f
{\displaystyle f}
T
{\displaystyle T}
f
{\displaystyle f}
G
f
(
x
,
y
)
{\displaystyle {\mathcal {G}}_{f}(x,\,y)}
⊢
T
(
∀
y
)
{
G
f
(
∘
#
A
,
y
)
⇔
[
y
=
∘
f
(
#
A
)
]
}
{\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y={}^{\circ }f(\#_{\mathcal {A}})]\}}
つまり
⊢
T
(
∀
y
)
{
G
f
(
∘
#
A
,
y
)
⇔
[
y
=
∘
#
(
A
(
∘
#
A
)
)
]
}
{\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\}}
ここで、1つの自由変数
y
{\displaystyle y}
F
(
y
)
{\displaystyle {\mathcal {F}}(y)}
B
(
z
)
{\displaystyle {\mathcal {B}}(z)}
B
(
z
)
:=
(
∀
y
)
[
G
f
(
z
,
y
)
⇒
F
(
y
)
]
{\displaystyle {\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]}
すると、1つの自由変数を持つ全ての式
A
(
x
)
{\displaystyle {\mathcal {A}}(x)}
⊢
T
B
(
∘
#
A
)
⇔
(
∀
y
)
{
[
y
=
∘
#
(
A
(
∘
#
A
)
)
]
⇒
F
(
y
)
}
{\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow (\forall y)\{[y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\Rightarrow {\mathcal {F}}(y)\}}
つまり
⊢
T
B
(
∘
#
A
)
⇔
F
(
∘
#
[
A
(
∘
#
A
)
]
)
{\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow {\mathcal {F}}(^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})])}
ここで、
A
{\displaystyle {\mathcal {A}}}
B
{\displaystyle {\mathcal {B}}}
C
{\displaystyle {\mathcal {C}}}
C
:=
B
(
∘
#
B
)
{\displaystyle {\mathcal {C}}:={\mathcal {B}}(^{\circ }\#_{\mathcal {B}})}
すると、前の行は以下のように書き直すことができる。
⊢
T
C
⇔
F
(
∘
#
C
)
{\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}
これが求める結果である。
(異なる用語による同じ議論は、Raatikainen (2015a)で与えられている。)
対角化定理はカントールの対角線論法 と類似しているため、「対角化」と呼ばれる[ 5] クルト・ゲーデル の1931年の論文 （英語版 ） アルフレト・タルスキ の1936年の論文 には登場しない。
ルドルフ・カルナップ (1934)は、一般自己言及補題 （general self-reference lemma）を最初に証明した[ 6] T における任意の式F に対して、ψ ↔ F (°#(ψ ))がT で証明可能であるような式ψ が存在することを述べている。カルナップの研究は異なる用語で表現されていた。なぜなら、計算可能関数 の概念は1934年にはまだ開発されていなかったからである。メンデルソン （英語版 ） [ 7]
対角化定理は、計算可能性理論 におけるクリーネの再帰定理 と密接に関連しており、それぞれの証明は類似している。
^ Hájek, Petr; Pudlák, Pavel (1998). Metamathematics of First-Order Arithmetic . Perspectives in Mathematical Logic (1st ed.). Springer. ISBN 3-540-63648-X . ISSN 0172-6641 . "In modern texts these results are proved using the well-known diagonalization (or self-reference) lemma, which is already implicit in Gödel's proof." ^ Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 )を参照のこと。
^ 表現可能性の詳細については、Hinman 2005, p. 316を参照のこと
^ Smullyan (1991, 1994)は標準的な専門書である。定理はMendelson (1997)のProp. 3.34であり、Boolos and Jeffrey (1989, sec. 15)やHinman (2005)などの基本的な数理論理学に関する多くのテキストで取り上げられている。
^ 例えば、Gaifman (2006)を参照のこと。
^ Kurt Gödel , Collected Works, Volume I: Publications 1929–1936 , Oxford University Press, 1986, p. 339.^ ゲーデルのCollected Works, Vol. 1 , Oxford University Press, 1986, p. 363, fn 23を参照のこと。
^ 英語等では補題とするのが一般的であるが、日本語では対角化定理と呼ぶことが多い。
^ 文の同値類とは、理論
T
{\displaystyle T}
George Boolos and Richard Jeffrey , 1989. Computability and Logic , 3rd ed. Cambridge University Press. ISBN 0-521-38026-X ISBN 0-521-38923-2 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. ISBN 1-56881-262-0
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
Alfred Tarski (1936). “Der Wahrheitsbegriff in den formalisierten Sprachen” . Studia Philosophica 1 : 261–405. オリジナル の9 January 2014時点におけるアーカイブ。. https://web.archive.org/web/20140109135345/http://www.ifispan.waw.pl/studialogica/s-p-f/volumina_i-iv/I-07-Tarski-small.pdf 2013年6月26日閲覧。 . 
![{\displaystyle \vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {G}}_{f}(^{\circ }n,\,y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c0caabb4aa4743a78fec9b30042d7546a4fa818)
![{\displaystyle f(\#_{\mathcal {A}})=\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/689b7b31a90538e252eeb313b21e4513b1748c39)
![{\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y={}^{\circ }f(\#_{\mathcal {A}})]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7b8d58ec09b5a5ebb0e8ffadbe3244b6efb53a4c)
![{\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/74aad42d8a573be2a750a8f6636686262a767f40)
![{\displaystyle {\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d11d08c15ee61357d0fc35c4c9e6672c059f307)
![{\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow (\forall y)\{[y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\Rightarrow {\mathcal {F}}(y)\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/31ee7caefca1a58c8c3e1a44e6303c0d1b2a77b9)
![{\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow {\mathcal {F}}(^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/17991b52117e29c5c721fa6a14ad0e298bb04f78)
