ケーニヒの補題

グラフ理論におけるケーニヒの補題はデネス・ケーニヒ^[1] (1936)によって示された定理で、無限グラフが無限長の道をもつための十分条件を与える。この定理のcomputability aspectsは数理論理学の計算可能性理論の研究者によって調べられてきている。この定理は構成的数学や証明論においても重要な役割をもつ。

定理の内容[編集]

Gを無限個の点からなる連結グラフで全ての点の次数は有限（すなわちどの点も他の有限個の点としか接続していない）とする。このとき、Gは無限長の単純道（同じ点を2度通らない道）を持つ。

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

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

証明[編集]

証明にあたって、グラフの含む無限個の各点を v_i の形で表し、グラフは連結であるとする。

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

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

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

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

構成的数学やコンパクト性との関連[編集]

ブラウワーのfan定理^[2] は伝統的な見方によるとケーニヒの補題と対照的である。 $\{0,1\}^{<\omega }\,$ の部分集合 S が bar であるとは、 $\omega$ から $\{0,1\}$ への任意の関数の始切片が S の要素になっていること。 barが 分離できる とは、任意の列がbarの要素か、barの要素でないかであること。（この用語を定義するのはこの定理が排中律を仮定しない状況で使用されるからである。） barが一様であるとは、ある数 N が存在して、いかなる $\omega$ から $\{0,1\}$ への関数も始切片をbarの長さ $N$ 以下の要素として持つこと。ブラウワーのfan定理は、分離できないbarは一様なbarであることを主張する。

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

選択公理との関連[編集]

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

グラフが可算であるなら、点は整列集合を成し、適切な点のうち最小のものを canonical に選ぶことができる。この場合、ケーニヒの補題は二階算術(en)の算術的内包公理 ${\mbox{ACA}}_{0}\,$ を使って証明できる。ZF集合論を用いるなら尚更のことである（選択公理は不要）。

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

参照[編集]

^ 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.
^ Brouwer, L. E. J. (1927). "On the Domains of Definition of Functions", published in Jean van Heijenoort, editor, From Frege to Gödel, 1967.

Cenzer, D. (1999). " $\Pi _{1}^{0}$ classes in recursion theory". Handbook of Computability Theory. Elsevier. pp. 37–85. ISBN 0444898824。
König, D. (1926年). “Sur les correspondances multivoques des ensembles”. Fundamenta Mathematicae, (8): pp. 114–134
Kőnig, D. (1936). Theorie der Endlichen und Unendlichen Graphen: Kombinatorische Topologie der Streckenkomplexe. Leipzig: Akad. Verlag
Levy, A. (1979). Basic Set Theory. Springer Reprint Dover 2002, ISBN 0486420795.
Rogers, H. (1967). Theory of Recursive Functions and Effective Computability
Simpson, S. (1999). Subsystems of Second Order Arithmetic. Springer
Soare, R. (1987). Recursively Enumerable Sets and Degrees. Springer
Truss, J. (1976). “Some cases of König's lemma”. In Marek, Srebrny, and Zarach. Set theory and hierarchy theory. Lecture notes in mathematics. 537. pp. 273–284

外部リンク[編集]

Stanford Encyclopedia of Philosophy: Constructive Mathematics
Weisstein, Eric W. "König's Lemma". mathworld.wolfram.com (英語).
The Mizar project has completely formalized and automatically checked the proof of a version of König's lemma in the file TREES_2.

[1] 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.

[2] Brouwer, L. E. J. (1927). "On the Domains of Definition of Functions", published in Jean van Heijenoort, editor, From Frege to Gödel, 1967.

[1]

[2]