ケーニヒの補題のソースを表示

[[グラフ理論]]における'''ケーニヒの補題'''は[[デネス・ケーニヒ]]<ref>Note that, although Kőnig's name is properly spelled with a [[double acute accent]], the lemma named after him is customarily spelled with an umlaut.</ref> (1936)によって示された定理で、
無限グラフが無限長の道をもつための十分条件を与える。
この定理のcomputability aspectsは[[数理論理学]]の[[計算可能性理論]]の研究者によって調べられてきている。
この定理は[[構成的数学]]や[[証明論]]においても重要な役割をもつ。

==定理の内容==
[[File:Lemme de konig.svg|thumb|200px|局所有限な無限連結グラフは無限長の単純道を持つ。]]
''G''を[[無限]]個の点からなる[[連結グラフ]]で全ての点の次数は有限（すなわちどの点も他の有限個の点としか接続していない）とする。
このとき、''G''は無限長の[[道 (グラフ理論)|単純道]]（同じ点を2度通らない道）を持つ。

[[木 (数学)|木]]に対して制限したバージョンがこの定理の特殊な例としてよく知られている。

次数は有限である必要があるが有界である必要はないことに注意。すなわち各点の次数が10,100,1000…という増加列を構成していてもよい。

===証明===

証明にあたって、グラフの含む無限個の各点を ''v''<sub>i</sub> の形で表し、グラフは連結であるとする。

''v''<sub>1</sub> を任意にとる。グラフの無限個の点が ''v''<sub>1</sub> からの単純道で到達でき、
そのような道はいずれも ''v''<sub>1</sub> に接続する有限個の点のうちどれかから始まる。
そのような点のうち、その点から無限個の点に ''v''<sub>1</sub> を通らない道で到達できるようなものがある
（もしそのような点がなかったらグラフの全体が有限集合の有限和であり、グラフが無限であることに反する。）
ここで、そのような点を一つとって ''v''<sub>2</sub> とする。

今、グラフの無限個の点が ''v''<sub>2</sub> からの ''v''<sub>1</sub> を通らない単純道で到達できる。
そのような道はいずれも ''v''<sub>2</sub> に接続する有限個の点のうちどれかから始まる。
上で行ったのと同様の議論により、無限個の点に到達できる道の始点をとって ''v''<sub>3</sub> とする。

同様の議論を続ける[[数学的帰納法]]により、無限単純道が得られる。
各ステップで帰納法の仮定は、 ''v''<sub>i</sub> から始まる一つの単純道で、
ある有限集合を通らずに無限個の点に到達できるということであり、
帰納法の議論は ''v''<sub>i</sub> をその有限集合に加えてもある隣接点が帰納法の仮定を満たすことにより成り立つ。
同じ点が二度追加されないことも構成法から保証されていて結果として、
任意の ''n'' に対して所望の道を成す ''v''<sub>''n''</sub> が選べる。

この証明は構成的でないとされることがある。というのは、
各ステップで、無限個の点に到達できる隣接点が存在することを[[背理法]]で示してあり、
この補題のcomputational aspectsが、
[[構成的数学]]の主流から言って構成的と思える証明が存在しないことを示唆しているからである。


==構成的数学やコンパクト性との関連==

[[ライツェン・エヒベルトゥス・ヤン・ブラウワー|ブラウワー]]のfan定理<ref>Brouwer, L. E. J. (1927). "On the Domains of Definition of Functions", published in Jean van Heijenoort, editor, ''From Frege to Gödel'', 1967.</ref>
は伝統的な見方によるとケーニヒの補題と対照的である。
<math>\{0,1\}^{<\omega}\,</math> の部分集合 ''S'' が ''bar'' であるとは、<math>\omega</math> から <math>\{0,1\}</math> への
任意の関数の始切片が ''S'' の要素になっていること。
barが ''分離できる'' とは、任意の列がbarの要素か、barの要素でないかであること。
（この用語を定義するのはこの定理が排中律を仮定しない状況で使用されるからである。）
barが ''一様'' であるとは、ある数 ''N'' が存在して、いかなる <math>\omega</math> から <math>\{0,1\}</math> への関数も
始切片をbarの長さ <math>N</math> 以下の要素として持つこと。
ブラウワーのfan定理は、分離できないbarは一様なbarであることを主張する。

この定理は、barを[[コンパクト空間]] <math>\{0,1\}^\omega</math> の開被覆と見なすことにより示される。
barの要素である列はこの空間の開基であり、これらの開基は空間を被覆する。
コンパクト性により、この被覆は有限部分被覆を持つ。
fan定理の ''N'' を有限部分被覆の要素である開基のうち最長列の長さとして取ればよい。
この位相的な証明は、次のケーニヒの補題の変形にも通用する。：任意自然数 ''k'' に対し、
<math>\{0,\ldots,k\}^{<\omega}\,</math> のいかなる無限部分木も無限な道をもつ。

==選択公理との関連==

ケーニヒの補題は選択の原理であるとも言える。上述の一つめの証明はこの補題と[[従属選択公理]]との関係を表している。帰納法の各ステップにおいて、ある特別な性質を持った点を選ばなければならない。そのような性質を満たす点が少なくとも一つ存在することが証明されているが、もし適切な点が一つよりも多く存在するときは、その内の一つを canonical に選択する方法はない。

グラフが可算であるなら、点は[[整列集合]]を成し、適切な点のうち最小のものを canonical に選ぶことができる。この場合、ケーニヒの補題は[[二階算術]]([[:en:Second-order arithmetic|en]])の[[逆数学#算術的内包公理|算術的内包公理]] <math>\mbox{ACA}_0 \, </math>を使って証明できる。[[ツェルメロ＝フレンケルの公理系|ZF]]集合論を用いるなら尚更のことである（[[選択公理]]は不要）。

ケーニヒの補題は本質的に、dependent choice の公理を、各 ''x'' に対して ''xRz'' となる ''z'' が有限個しか存在しないような entire relation ''R'' に制限するものである。選択公理は一般には dependent choice の原理より強いが、この dependent choice の制限と選択公理の制限は同じものになる。特に各点が、可算とは限らない任意の集合の有限部分集合上で分岐する場合、ケーニヒの補題の言う"有限分岐する無限木は無限パスをもつ" は、有限集合の可算集合は全て選択関数を持つという原理と同値になる(Truss (1976:273); Levy (1979, Exercise IX.2.18)と比較せよ)。この形の選択公理は（すなわちケーニヒの補題も）ZFの下では証明できない。

==関連項目==
* [[アロンシャイン木]]は、ケーニヒの補題をより大きな基数へと一般化する場合に、その反例となりうる木である。

==参照==
{{reflist}}
*{{cite conference
 | author = Cenzer, D.
 | title = <math>\Pi^0_1</math> classes in recursion theory
 | book-title = Handbook of Computability Theory
 | publisher = Elsevier
 | date = 1999
 | pages = 37&ndash;85
 | id = ISBN 0444898824}}
*{{cite article
 | author = König, D.
 | title = Sur les correspondances multivoques des ensembles
 | url = http://matwbn.icm.edu.pl/ksiazki/fm/fm8/fm815.pdf
 | journal = Fundamenta Mathematicae,
 | number = 8
 | year = 1926
 | pages = 114&ndash;134}}
*{{cite book
 | author = Kőnig, D.
 | authorlink = Dénes Kőnig
 | title = Theorie der Endlichen und Unendlichen Graphen: Kombinatorische Topologie der Streckenkomplexe
 | location = Leipzig
 | publisher = Akad. Verlag
 | year = 1936}}
*{{cite book
 | author = Levy, A.
 | title = Basic Set Theory
 | year = 1979
 | publisher = Springer}} Reprint Dover 2002, ISBN 0486420795.
*{{cite book
 | author = Rogers, H.
 | title = Theory of Recursive Functions and Effective Computability
 | year = 1967}}
*{{cite book
 | author = Simpson, S.
 | title = Subsystems of Second Order Arithmetic
 | publisher = Springer
 | year = 1999}}  
*{{cite book
 | author = Soare, R.
 | title = Recursively Enumerable Sets and Degrees
 | publisher = Springer
 | year = 1987}}
*{{cite book
  | author = Truss, J.
  | editor = Marek, Srebrny, and Zarach
  | chapter = Some cases of  König's lemma
  | year = 1976
  | title=Set theory and hierarchy theory
  | series = Lecture notes in mathematics
  | volume = 537
  | pages=273&ndash;284
}}

==外部リンク==
* [http://plato.stanford.edu/entries/mathematics-constructive/ Stanford Encyclopedia of Philosophy: Constructive Mathematics]
* {{Mathworld | title = König's Lemma | urlname = KoenigsLemma}} 
* The [[Mizar system|Mizar project]] has completely formalized and automatically checked the proof of a version of König's lemma in the file [http://mizar.org/JFM/Vol3/trees_2.html TREES_2].

{{DEFAULTSORT:けえにひのほたい}}
[[Category:補題]]
[[Category:証明を含む記事]]
[[Category:計算可能性理論]]
[[Category:整礎性]]
[[Category:選択公理]]
[[Category:グラフ理論]]
[[Category:無限グラフ]]
[[Category:数学に関する記事]]