ブーフホルツのヒドラ

ヒドラゲームも参照して下さい。

ブーフホルツのヒドラ (Buchholz's hydra) は、ラベル付き木を使って行う一人用 (あるいは二人用) ゲームである。このゲームから定義される関数を \(\text{BH}(n)\)とする。この関数の増加率は竹内・フェファーマン・ブーフホルツ順序数で表される。

準備[]

ブーフホルツのヒドラで使う用語の定義を行う。

(単純) グラフとは、次の条件を満たす集合\(V,E\)の組\(G=(V,E)\)である：

\(E\)の要素は全て、\(V\)の異なる2つの要素からなる集合である。すなわち、
\(\forall e\in E.\exists v,w\in V.(v\neq w)\land(e=\{v,w\})\)

グラフ\(G=(V,E)\)に対して、\(V\)の要素を\(G\)の頂点、\(E\)の要素を\(G\)の辺という。

集合\(L\)を、\(L=\mathbb{N}\cup\{\omega,\mathord{+}\}\)で定義する。ブーフホルツのヒドラゲームには頂点が\(L\)でラベルされた有限根付き木という特別なグラフを用いる。すなわち、

有限: \(V,E\)はいずれも有限集合である。
木: 任意の2つの頂点が、ただ1つの道で繋がっている。つまり、任意の\(v,w\in V\ (v\neq w)\)に対してある\(v_0,\dots,v_n\)と\(e_1,\dots,e_n\)が存在して\(e_i=\{v_{i-1},v_i\},v_0=v,v_n=w\)が成り立ち、そのような\(v_i,e_i\)がただ1つしか存在しないことが成り立つ。
根付き木: 木であって、さらに根と呼ばれる特別な頂点\(r\in V\)が指定されている。
頂点が\(L\)でラベルされた: グラフの各頂点に対して\(L\)の要素を対応させる写像\(\ell:V\to L\)が定められている。

が成り立つグラフを用いる。定義から、ラベルされた有限根付き木は頂点の集合、辺の集合、根、ラベルの組\(T=(V,E,r,\ell)\)によって表される。ヒドラゲームにおいて有限根付き木を図示する際は、根は他の頂点よりも下側に置かれ、枝分かれしながら上部に辺が伸びるように描かれる。この姿をヒュドラーに見立てて、ブーフホルツのヒドラゲームで用いる\(L\)でラベルされた有限根付き木をヒドラと呼ぶ。また、ヒュドラーの伝説になぞらえて、プレーヤーはヘラクレスと呼ばれる。

ヒドラは、頂点が\(L\)でラベルされた有限根付き木であって、さらに以下の条件を満たすものである：

根のラベルは\(\mathord{+}\)である。
根以外の頂点のラベルは、自然数または\(\omega\)である。
根に隣接した頂点のラベルは全て\(0\)である。

木において、辺が1つしか接続していない頂点を葉と呼ぶ。根でない葉をヒドラの頭、あるいはトップノード (top node)、頭とそこに接続した辺を合わせてヒドラの首 (head)と呼ぶことにする。また、首が接続している頂点をその首の根本と呼ぶことにする。あるヒドラの首が根から直接生えていないならば、首の根本からさらに根の方へ向かう辺がただ1つ存在している。そこでこれを親首と呼ぶことにする。

規則[]

ターンごとに、ヘラクレスはヒドラの首を1つ選び、それを切り落とす (グラフから除去する)。また、ヒドラは任意の自然数\(n\)を1つ選ぶ (例えば、現在のターン数など)。選んだヒドラの首と自然数に応じて、ヒドラは以下の規則に応じて変形する。

切った頭のラベルが0である場合。この時はヒドラゲームと同様にする。すなわち：
- 切った首の根本が根である場合、首は生えてこない。
- 切った首の根本が根でない場合、親首から上側のコピーが、親首の根本から\(n\)本新たに生える。
切った頭のラベルが0でない自然数\(u+1\)である場合。
1. ラベルが\(u\)以下である、切った頭から根に向かって最初の頂点を\(\rho\)とする。また、頂点\(\rho\)のラベルを\(v\)とする。
2. ヒドラの\(\rho\)から上の部分を\(S\)とする。\(S\)で\(\rho\)にあたる頂点のラベルを\(u\)にして、切った首が生えていた場所にラベルが0の頭を生やしたものを、元のヒドラの切った首の根本から生やす。
切った頭のラベルが\(\omega\)である場合、切った首の根本からラベルが\(n+1\)である頭が生える。

全てのヒドラの首を切り落として根だけにすることができればヘラクレスの勝利となる。ヒドラに対してどの首を落とすかの対応を戦略と呼び、その戦略によってヘラクレスが勝つならばそれを勝つ戦略、そうでないならば負ける戦略と呼ぶ。

ヒドラ定理[]

ブーフホルツは右端の葉を選び続ける戦略が勝つ戦略であることを示した。その証明において、ブーフホルツは「ヒドラから無限整礎木への標準的な対応が基本列を保つ」という性質を示しているが、ここから直接は「戦略には勝つ戦略しかない」という定理は従わない。この定理をヒドラ定理という。ヒドラ定理は\(\Pi_1^1\)-\(\text{CA}\)+\(\text{BI}\)で証明不可能であり、より強い集合論での証明も明示的に記述されたものは存在しないかもしれない。Googology Wikiにおいてブーフホルツがヒドラ定理を証明したと記載されていたが、少なくとも引用元では証明されていない。

ヒドラ定理には無限のヒドラは適用不可能である;次を見よ、section

\(\text{BH}(n)\)関数[]

\(x\)の辺をもち、\(+,0,\omega,\omega,...,\omega\)とラベルされている木を作る。その木を\(R^n\)とする。全ての\(x\)に対し\(\Pi_1^1\)-\(\text{CA}\)+\(\text{BI}\)では証明できないが、\(R^x(1)(2)(3)...(k)\)が根のみの木となる\(k\)が必ず存在する。(ここでの記法は、\(R^x\)を取り、\(n = 1\)、\(n = 2\)、\(n = 3\)、…、\(n = k\)で変形することを表す。)

\(\text{BH}(x)\)を\(R^x(1)(2)(3)...(k)\)が根のみの木となるような\(k\)とする。ヒドラ定理によりこの関数は定義可能である。\(\Pi_1^1\)-\(\text{CA}\)+\(\text{BI}\)でこの関数の全域性は証明できないと推測される。実際ブーフホルツは\(\lambda n.H_{D_0D_\nu^n0(1)}\)というヒドラから誘導される関数が\(\mathsf{ID}_\nu\)にて可証全域ではないことを示した．よってこの成長率は\(f_{\psi_0(\varepsilon_{\Omega_\omega + 1})}(x)\)に匹敵すると信じられている。ここで\(\psi\)はブーフホルツのψ関数であり、\(\psi_0(\varepsilon_{\Omega_\omega + 1})\)は竹内・フェファーマン・ブーフホルツ順序数である。驚くべきことではないが、この順序数は\(\Pi_1^1\)-\(\text{CA}\)+\(\text{BI}\)の証明論的順序数である。

BHの最初の二つの値は簡単に示される:\(\text{BH}(1) = 0\)、\(\text{BH}(2) = 1\)である。\(\text{BH}(3)\)はとても巨大で、いくらかの最初の操作の過程は右上に画像で示されている。

ブーフホルツのヒドラは計算可能な関数の中でも強い関数の一つである。TREE(n)、そしてSCG(n)を超えるだろうと予測されている。loader.cや、有限約束ゲーム、レイバーのテーブルからなる数よりは小さいだろうし、計算可能なため、ビジービーバー関数よりも小さい。

出典や参考[]

W. Buchholz, "An independence result for \(\Pi_1^1\)-\(\text{CA}\)+\(\text{BI}\)". Annals of Pure and Applied Logic, Vol. 33, pp. 131–155 (1987). doi:10.1016/0168-0072(87)90078-9
M. Hamano, M. Okada, A relationship among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game, Math. Logic Quart. 43 (1997) 103-120.
M. Hamano, M. Okada, A direct independence proof of Buchholz's Hydra Game on finite labeled trees, Arch. Math. Logic 37 (1998) 67-89.
L. Kirby, J. Paris, Accessible independence results for Peano Arithmetic, Bull. Lon. Math. Soc. 14 (1982) 285-293.
J. Ketonen, R. Solovay, Rapidly growing Ramsey functions, Ann. Math. 113 (1981) 267-314.
G. Takeuti, Proof Theory, 2nd Edition, North-Holland, Amsterdam, 1987.