対角化定理のソースを表示

{{Otheruses|数理論理学における概念|名前の元になった証明テクニック|カントールの対角線論法|行列の対角行列への変形|対角化}}

[[数理論理学]]では、'''対角化定理'''{{Efn|英語等では補題とするのが一般的であるが、日本語では対角化定理と呼ぶことが多い。}}（対角線補題（diagonal lemma）、対角化補題（diagonalization lemma）、自己言及補題（self-reference lemma）<ref>{{cite book
| last1        = Hájek
| first1       = Petr
| author-link1 = Petr Hájek
| last2        = Pudlák
| first2       = Pavel
| year         = 1998
| orig-year    = first printing 1993
| edition      = 1st
| title        = Metamathematics of First-Order Arithmetic
| publisher    = Springer
| isbn         = 3-540-63648-X
| issn         = 0172-6641
| series       = Perspectives in Mathematical Logic
| quote        = 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.
}}</ref>または不動点定理（fixed point theorem）としても知られる）は、[[自然数]]の特定の形式理論、特にすべての[[計算可能関数]]を表すのに十分な強力な理論における、[[自己言及]]的{{仮リンク|文 (数理論理学)|en|Sentence (mathematical logic)|label=文}}の存在を示す定理である。対角化定理によって存在が保証される文は、[[ゲーデルの不完全性定理]]や[[タルスキの定義不可能性定理]]などの基本的な限界を証明するために使用できる<ref>Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 )を参照のこと。</ref>。

== 背景 ==
<math>\mathbb{N}</math>を[[自然数]]の集合とする。算術の言語における[[一階述語論理|一階]]{{仮リンク|理論 (数理論理学)|en|Theory (mathematical logic)|label=理論}} <math>T</math>は、計算可能関数<math>f: \mathbb{N}\rightarrow\mathbb{N}</math>について、もし<math>T</math>の言語における「グラフ」[[一階述語論理#論理式|論理式]]<math>\mathcal{G}_f(x, y)</math>が存在し、各<math>n \in \mathbb{N}</math>に対して以下が成り立つ場合に、<math>f</math>を''表現''（represent）<ref>表現可能性の詳細については、Hinman 2005, p. 316を参照のこと</ref>する。
: <math>\vdash_{T}\,(\forall y)[(^\circ f(n)=y) \Leftrightarrow \mathcal{G}_f(^\circ n,\,y)]</math>.
ここで、<math>{}^\circ n</math>は自然数<math>n</math>に対応する[[ペアノの公理#ペアノ算術|数詞]]（numeral）であり、<math>T</math>における最初の数詞<math>0</math>の<math>n</math>番目の後者（successor）と定義される。

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

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

== 定理のステートメント ==
{{math theorem|<math>T</math>を算術の言語における[[一階述語論理|一階]]理論であって全ての[[計算可能関数]]を表せるものとし、<math>\mathcal{F}(y)</math>を<math>T</math>における論理式であって1つの自由変数を持つものとする。すると、以下のような{{仮リンク|文 (数理論理学)|en|Sentence (mathematical logic)|label=文}}<math>\mathcal{C}</math>が存在する。
:<math>\vdash_T\,\mathcal{C}\Leftrightarrow\mathcal{F}({}^{\circ}\#_{\mathcal{C}})</math>
| name = 定理<ref>Smullyan (1991, 1994)は標準的な専門書である。定理はMendelson (1997)のProp. 3.34であり、Boolos and Jeffrey (1989, sec. 15)やHinman (2005)などの基本的な数理論理学に関する多くのテキストで取り上げられている。</ref>
}}

直感的には、<math>\mathcal{C}</math>は[[自己言及]]的文である。<math>\mathcal{C}</math>は、<math>\mathcal{C}</math>が性質<math>\mathcal{F}</math>を持つことを述べている。また、文<math>\mathcal{C}</math>は、与えられた文<math>\mathcal{A}</math>の同値類に対して、文<math>\mathcal{F}(^\circ \#_{\mathcal{A}})</math>の同値類を割り当てる操作の[[不動点]]と見なすこともできる{{Efn|文の同値類とは、理論<math>T</math>において論理的に同値なすべての文の集合である。}}(文の同値類とは、理論<math>T</math>において論理的に同値なすべての文の集合である)。証明の中で構成された文<math>\mathcal{C}</math>は、<math>\mathcal{F}(^\circ \#_{\mathcal{C}})</math>と字面上は同じではないが、理論<math>T</math>において論理的に同値である。

==証明==
<math>f:\mathbb{N}\to\mathbb{N}</math>を、理論<math>T</math>における1つの自由変数<math>x</math>のみを持つ各論理式<math>\mathcal{A}(x)</math>に対して以下のように定義された関数とする。
:<math>f(\#_{\mathcal{A}}) = \#[\mathcal{A}(^{\circ}\#_{\mathcal{A}})]</math>
ただし、<math>\#_{\mathcal{A}}=\#(\mathcal{A}(x))</math>は式<math>\mathcal{A}(x)</math>のゲーデル数を表す。また、<math>\#_{\mathcal{A}}</math>以外の<math>n</math>に対しては<math>f(n)=0</math>とする。この関数<math>f</math>は計算可能である(これは根源的にはゲーデル数の割り当て方法（Gödel numbering scheme）に関する仮定である)ので、<math>T</math>において<math>f</math>を表す式<math>\mathcal{G}_f(x,\,y)</math>が存在する。すなわち
:<math>\vdash_T\,(\forall y)\{\mathcal{G}_f(^{\circ}\#_{\mathcal{A}},\,y) \Leftrightarrow [y = {}^{\circ}f(\#_{\mathcal{A}})]\}</math>
つまり
:<math>\vdash_T\,(\forall y)\{\mathcal{G}_f(^{\circ}\#_{\mathcal{A}},\,y) \Leftrightarrow [y = {}^{\circ}\#(\mathcal{A}(^{\circ}\#_{\mathcal{A}}))]\}</math>
ここで、1つの自由変数<math>y</math>を持つ任意の式<math>\mathcal{F}(y)</math>が与えられたとき、式<math>\mathcal{B}(z)</math>を以下のように定義する。
:<math>\mathcal{B}(z) := (\forall y) [\mathcal{G}_f(z,\,y)\Rightarrow \mathcal{F}(y)]</math>
すると、1つの自由変数を持つ全ての式<math>\mathcal{A}(x)</math>に対して以下が成り立つ。
:<math>\vdash_T\,\mathcal{B}(^{\circ}\#_{\mathcal{A}}) \Leftrightarrow (\forall y)\{[ y = {}^{\circ}\#(\mathcal{A}(^{\circ}\#_{\mathcal{A}}))] \Rightarrow \mathcal{F}(y)\}</math>
つまり
:<math>\vdash_T\,\mathcal{B}(^{\circ}\#_{\mathcal{A}}) \Leftrightarrow \mathcal{F}(^{\circ}\#[\mathcal{A}(^{\circ}\#_{\mathcal{A}})])</math>
ここで、<math>\mathcal{A}</math>を<math>\mathcal{B}</math>に置き換え、文<math>\mathcal{C}</math>を以下のように定義する。
:<math>\mathcal{C}:= \mathcal{B}(^{\circ}\#_{\mathcal{B}})</math>
すると、前の行は以下のように書き直すことができる。
:<math>\vdash_T\,\mathcal{C}\Leftrightarrow\mathcal{F}(^{\circ}\#_{\mathcal{C}})</math>
これが求める結果である。

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

==歴史<!--'General self-referential lemma' redirects here-->==
対角化定理は[[カントールの対角線論法]]と類似しているため、「対角化」と呼ばれる<ref>例えば、Gaifman (2006)を参照のこと。</ref>。「対角化定理」または「不動点」という用語は、[[クルト・ゲーデル]]の{{仮リンク|プリンキピア・マテマティカとその関連体系における形式的に決定不可能な命題について|en|On Formally Undecidable Propositions of Principia Mathematica and Related Systems|label=1931年の論文}}や[[アルフレト・タルスキ]]の[[タルスキの定義不可能性定理|1936年の論文]]には登場しない。

[[ルドルフ・カルナップ]] (1934)は、'''一般自己言及補題'''<!--boldface per WP:R#PLA-->（general self-reference lemma）を最初に証明した<ref>[[クルト・ゲーデル|Kurt Gödel]], ''Collected Works, Volume I: Publications 1929–1936'', Oxford University Press, 1986, p. 339.</ref>。これは、特定の条件を満たす理論''T''における任意の式''F''に対して、ψ ↔ ''F''(°#(''ψ''))が''T''で証明可能であるような式''ψ''が存在することを述べている。カルナップの研究は異なる用語で表現されていた。なぜなら、[[計算可能関数]]の概念は1934年にはまだ開発されていなかったからである。{{仮リンク|エリオット・メンデルソン|en|Elliott Mendelson|label=メンデルソン}}（1997, p. 204）は、対角化定理のようなものがゲーデルの推論に暗黙的に含まれていると述べたのはカルナップが最初であると信じている。ゲーデルは1937年までにはカルナップの研究を知っていた<ref>ゲーデルの''Collected Works, Vol. 1'', Oxford University Press, 1986, p. 363, fn 23を参照のこと。</ref>。

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

==関連項目==
*{{仮リンク|間接的自己言及|en|Indirect self-reference}}
*[[不動点定理#各種の不動点定理|不動点定理の一覧]]
*[[原始帰納的算術]]
*[[自己言及]]
*[[自己言及のパラドックス]]

==脚注==
===出典===
{{Reflist}}
=== 注釈 === 
{{Notelist}}
==参考文献==
* [[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. '[https://haimgaifman.files.wordpress.com/2016/07/22odel-to-kleene.pdf 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}}
* [[Elliott Mendelson|Mendelson, Elliott]], 1997. ''Introduction to Mathematical Logic'', 4th ed. Chapman & Hall.
* Panu Raatikainen, 2015a. [http://plato.stanford.edu/entries/goedel-incompleteness/sup2.html The Diagonalization Lemma].  In [[Stanford Encyclopedia of Philosophy]], ed. Zalta.  Supplement to Raatikainen (2015b).
* Panu Raatikainen, 2015b. [http://plato.stanford.edu/entries/goedel-incompleteness/index.html 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. ''[https://philpapers.org/rec/SMUDAS Diagonalization and Self-Reference]''. Oxford Univ. Press.
* {{cite journal| author=Alfred Tarski| author-link=アルフレト・タルスキ| title=Der Wahrheitsbegriff in den formalisierten Sprachen| journal=[[Studia Philosophica (Poland)|Studia Philosophica]]| year=1936| volume=1| pages=261–405| url=http://www.ifispan.waw.pl/studialogica/s-p-f/volumina_i-iv/I-07-Tarski-small.pdf| accessdate=26 June 2013| url-status=dead| archiveurl=https://web.archive.org/web/20140109135345/http://www.ifispan.waw.pl/studialogica/s-p-f/volumina_i-iv/I-07-Tarski-small.pdf| archivedate=9 January 2014}}
** [[アルフレト・タルスキ|Alfred Tarski]], tr. J. H. Woodger, 1983. "The Concept of Truth in Formalized Languages". [http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Tarski%20-%20The%20Concept%20of%20Truth%20in%20Formalized%20Languages.pdf English translation of Tarski's 1936 article].  In A. Tarski, ed. J. Corcoran, 1983, ''Logic, Semantics, Metamathematics'', Hackett.

{{DEFAULTSORT:たいかくかていり}}
[[Category:数理論理学]]
[[Category:補題]]
[[Category:証明を含む記事]]
[[Category:数学に関する記事]]