コンテンツにスキップ

英文维基 | 中文维基 | 日文维基 | 草榴社区

対角化定理

出典: フリー百科事典『ウィキペディア(Wikipedia)』
対角化補題から転送)

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

背景

[編集]

自然数の集合とする。算術の言語における一階理論英語版 は、計算可能関数について、もしの言語における「グラフ」論理式が存在し、各に対して以下が成り立つ場合に、表現(represent)[4]する。

.

ここで、は自然数に対応する数詞(numeral)であり、における最初の数詞番目の後者(successor)と定義される。

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

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

定理のステートメント

[編集]

定理[5] ― を算術の言語における一階理論であって全ての計算可能関数を表せるものとし、における論理式であって1つの自由変数を持つものとする。すると、以下のような英語版が存在する。

直感的には、自己言及的文である。は、が性質を持つことを述べている。また、文は、与えられた文の同値類に対して、文の同値類を割り当てる操作の不動点と見なすこともできる(文の同値類とは、理論において論理的に同値なすべての文の集合である)。証明の中で構成された文は、と字面上は同じではないが、理論において論理的に同値である。

証明

[編集]

を、理論における1つの自由変数のみを持つ各論理式に対して以下のように定義された関数とする。

ただし、は式のゲーデル数を表す。また、以外のに対してはとする。この関数は計算可能である(これは根源的にはゲーデル数の割り当て方法(Gödel numbering scheme)に関する仮定である)ので、においてを表す式が存在する。すなわち

つまり

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

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

つまり

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

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

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

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

歴史

[編集]

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

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

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

関連項目

[編集]

注釈

[編集]
  1. ^ 英語等では補題とするのが一般的であるが、日本語では対角化定理と呼ぶことが多い。
  2. ^ 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." 
  3. ^ Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 )を参照のこと。
  4. ^ 表現可能性の詳細については、Hinman 2005, p. 316を参照のこと
  5. ^ Smullyan (1991, 1994)は標準的な専門書である。定理はMendelson (1997)のProp. 3.34であり、Boolos and Jeffrey (1989, sec. 15)やHinman (2005)などの基本的な数理論理学に関する多くのテキストで取り上げられている。
  6. ^ 例えば、Gaifman (2006)を参照のこと。
  7. ^ Kurt Gödel, Collected Works, Volume I: Publications 1929–1936, Oxford University Press, 1986, p. 339.
  8. ^ ゲーデルのCollected Works, Vol. 1, Oxford University Press, 1986, p. 363, fn 23を参照のこと。

参考文献

[編集]