対角化定理

数理論理学では、対角化定理テンプレート:Efn（対角線補題（diagonal lemma）、対角化補題（diagonalization lemma）、自己言及補題（self-reference lemma）または不動点定理（fixed point theorem）としても知られる）は、自然数の特定の形式理論、特にすべての計算可能関数を表すのに十分な強力な理論における、自己言及的テンプレート:仮リンクの存在を示す定理である。対角化定理によって存在が保証される文は、ゲーデルの不完全性定理やタルスキの定義不可能性定理などの基本的な限界を証明するために使用できる。

背景

$\mathbb{N}$を自然数の集合とする。算術の言語における一階テンプレート:仮リンク $T$は、計算可能関数$f:\mathbb{N}\to \mathbb{N}$について、もし$T$の言語における「グラフ」論理式${𝒢}_f(x,y)$が存在し、各$n\in \mathbb{N}$に対して以下が成り立つ場合に、$f$を表現（represent）する。

${⊢}_T(\mathrm{\forall }y)[{(}^{\circ }f(n)=y)\iff {𝒢}_f{(}^{\circ }n,y)]$.

ここで、${}^{\circ }n$は自然数$n$に対応する数詞（numeral）であり、$T$における最初の数詞$0$の$n$番目の後者（successor）と定義される。

対角化定理はまた、すべての式$𝒜$に、そのゲーデル数と呼ばれる自然数$\mathrm{\#}(𝒜)$（${\mathrm{\#}}_{𝒜}$とも表記される）を割り当てる体系的な方法を必要とする。すると、式は$T$内でそのゲーデル数に対応する数詞によって表現できる。例えば、$𝒜$は${\circ }^{}{\mathrm{\#}}_{𝒜}$によって表現される。

対角化定理は、原始再帰関数を全て表せる理論に適用される。そのような理論には、一階ペアノ算術や、より弱いロビンソン算術、さらにはRとして知られるはるかに弱い理論も含まれる。定理の一般的なステートメント（後述）は、理論が全ての計算可能関数を表せるというより強い仮定を立てるが、前述の各理論はその能力を持っている。

定理のステートメント

直感的には、$𝒞$は自己言及的文である。$𝒞$は、$𝒞$が性質$ℱ$を持つことを述べている。また、文$𝒞$は、与えられた文$𝒜$の同値類に対して、文$ℱ{(}^{\circ }{\mathrm{\#}}_{𝒜})$の同値類を割り当てる操作の不動点と見なすこともできるテンプレート:Efn(文の同値類とは、理論$T$において論理的に同値なすべての文の集合である)。証明の中で構成された文$𝒞$は、$ℱ{(}^{\circ }{\mathrm{\#}}_{𝒞})$と字面上は同じではないが、理論$T$において論理的に同値である。

証明

$f:\mathbb{N}\to \mathbb{N}$を、理論$T$における1つの自由変数$x$のみを持つ各論理式$𝒜(x)$に対して以下のように定義された関数とする。

$f({\mathrm{\#}}_{𝒜})=\mathrm{\#}[𝒜{(}^{\circ }{\mathrm{\#}}_{𝒜})]$

ただし、${\mathrm{\#}}_{𝒜}=\mathrm{\#}(𝒜(x))$は式$𝒜(x)$のゲーデル数を表す。また、${\mathrm{\#}}_{𝒜}$以外の$n$に対しては$f(n)=0$とする。この関数$f$は計算可能である(これは根源的にはゲーデル数の割り当て方法（Gödel numbering scheme）に関する仮定である)ので、$T$において$f$を表す式${𝒢}_f(x,y)$が存在する。すなわち

${⊢}_T(\mathrm{\forall }y)\{{𝒢}_f{(}^{\circ }{\mathrm{\#}}_{𝒜},y)\iff [y={}^{\circ }f({\mathrm{\#}}_{𝒜})]\}$

つまり

${⊢}_T(\mathrm{\forall }y)\{{𝒢}_f{(}^{\circ }{\mathrm{\#}}_{𝒜},y)\iff [y={}^{\circ }\mathrm{\#}(𝒜{(}^{\circ }{\mathrm{\#}}_{𝒜}))]\}$

ここで、1つの自由変数$y$を持つ任意の式$ℱ(y)$が与えられたとき、式$ℬ(z)$を以下のように定義する。

$ℬ(z):=(\mathrm{\forall }y)[{𝒢}_f(z,y)\Rightarrow ℱ(y)]$

すると、1つの自由変数を持つ全ての式$𝒜(x)$に対して以下が成り立つ。

${⊢}_Tℬ{(}^{\circ }{\mathrm{\#}}_{𝒜})\iff (\mathrm{\forall }y)\{[y={}^{\circ }\mathrm{\#}(𝒜{(}^{\circ }{\mathrm{\#}}_{𝒜}))]\Rightarrow ℱ(y)\}$

つまり

${⊢}_Tℬ{(}^{\circ }{\mathrm{\#}}_{𝒜})\iff ℱ{(}^{\circ }\mathrm{\#}[𝒜{(}^{\circ }{\mathrm{\#}}_{𝒜})])$

ここで、$𝒜$を$ℬ$に置き換え、文$𝒞$を以下のように定義する。

$𝒞:=ℬ{(}^{\circ }{\mathrm{\#}}_{ℬ})$

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

${⊢}_T𝒞\iff ℱ{(}^{\circ }{\mathrm{\#}}_{𝒞})$

これが求める結果である。

(異なる用語による同じ議論は、Raatikainen (2015a)で与えられている。)

歴史

対角化定理はカントールの対角線論法と類似しているため、「対角化」と呼ばれる。「対角化定理」または「不動点」という用語は、クルト・ゲーデルのテンプレート:仮リンクやアルフレト・タルスキの1936年の論文には登場しない。

ルドルフ・カルナップ (1934)は、一般自己言及補題（general self-reference lemma）を最初に証明した。これは、特定の条件を満たす理論Tにおける任意の式Fに対して、ψ ↔ F(°#(ψ))がTで証明可能であるような式ψが存在することを述べている。カルナップの研究は異なる用語で表現されていた。なぜなら、計算可能関数の概念は1934年にはまだ開発されていなかったからである。テンプレート:仮リンク（1997, p. 204）は、対角化定理のようなものがゲーデルの推論に暗黙的に含まれていると述べたのはカルナップが最初であると信じている。ゲーデルは1937年までにはカルナップの研究を知っていた。

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

関連項目

• テンプレート:仮リンク
• 不動点定理の一覧
• 原始帰納的算術
• 自己言及
• 自己言及のパラドックス

参考文献

• George Boolos and Richard Jeffrey, 1989. Computability and Logic, 3rd ed. Cambridge University Press. テンプレート:ISBN テンプレート:ISBN
• 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
• 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.
• テンプレート:Cite journal
  • 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.