- Voir aussi: Hydre de Kirby-Paris
The Buchholz hydra game is a one-player game played on trees labelled with any finite number or ω. From the game arises a fast-growing function BH(n) which eventually dominates all recursive functions provably total in , and is itself provably total in + "transfinite induction with respect to TFB".
Rules
The game is played on a finite labelled tree \(T\) where the root is marked with a special label (call it +), and every child of root has label 0, and every other node is labeled by any ordinal \(\leq \omega\). This tree is called a hydra.
At each step, we choose a leaf node \(a\) to chop off. On the other hand, hydra chooses a nonnegative integer \(n\) in some way (for example, it is determined as the number of current step, starting from 1). The hydra alters by the following rules:
- If \(a\) has label 0, we proceed as in Kirby-Paris' game. Call the node's parent \(b\), and its grandparent \(c\) (if it exists). First we delete \(a\). If \(c\) exists (i.e. \(b\) is not the root), we make \(n\) copies of \(b\) and all its children and attach them to \(c\).
- If \(a\) has label \(u + 1\), we go down the tree looking for a node \(b\) with label \(v \leq u\) (which is guaranteed to exist, as every child of the root node has label 0). Consider the subtree rooted at \(b\) — call it \(S\). Create a copy of \(S\), call it \(S'\). Within \(S'\), we relabel \(b\) with \(u\) and relabel \(a\) with \(0\). Back in the original tree, replace \(a\) with \(S'\).
- If \(a\) has label \(\omega\), we simply relabel it with \(n + 1\).
If \(a\) is the hydra's rightmost leaf, we notate the transformed tree as \(T(n)\).
As we go about altering the hydra, we pick leaves. The sequence of leaves is called a strategy. A strategy is a winning strategy if it eventually leaves us with only the root node, and a losing strategy otherwise.
Hydra theorem
It was believed in this community that Wilfried Buchholz showed that there are no losing strategies for any hydra, but the source of this article does not include such a result. A similar made-up description is found in Kirby-Paris hydra#Hydra Theorem.
Call this statement the hydra theorem. What he actually showed is the canonical correspondence from a hydra to an infnitary well-founded tree (or the corresponding term in the notation system \(T\) associated to Buchholz's function, which does not necessarily belong to the ordinal notation system \(OT \subset T\)), preserves fundamental sequences, i.e. the strategy to choose the rightmost leaves and the \((n)\) operation on an infinitary well-founded tree (or the \([n]\) operation on the corresponding term in \(T\)). Although it might fortunately imply the hydra theorem under some weak set theory, the statement that he showed the hydra theorem is wrong because he even does not state the hydra theorem. He only refered to the fact that the sequence of the rightmost leaves is a winning strategy. The hydra theorem is unprovable in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\), but for individual hydras it was believed to be provable in this community without a source.
\(\text{BH}(n)\) function
Suppose we make a tree with just one branch with \(x\) nodes, labeled \(+,0,\omega,\omega,...,\omega\). Call such a tree \(R^n\). It cannotModèle:Citation needed be proven in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) that for all \(x\), there exists \(k\) such that \(R^x(1)(2)(3)...(k)\) is root tree. (The latter expression means taking the tree \(R^x\), then transforming it with \(n = 1\), then \(n = 2\), then \(n = 3\), etc. up to \(n = k\).)
Define \(\text{BH}(x)\) as the smallest \(k\) such that \(R^x(1)(2)(3)...(k)\) as defined above is root tree. By the hydra theorem this function is well-defined, but its totality cannot be proven in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\). Its rate of growth is believed to be comparable to \(f_{\psi_0(\varepsilon_{\Omega_\omega + 1})}(x)\) with respect to unspecified system of fundamental sequences without a proof. Here \(\psi\) denotes Buchholz's function, and (\(\psi_0(\varepsilon_{\Omega_\omega + 1})\) is the Takeuti-Feferman-Buchholz ordinal, which unsurprisingly measures the strength of \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).)
The first two values of the BH function are virtually degenerate: \(\text{BH}(1) = 0\) and \(\text{BH}(2) = 1\). \(\text{BH}(3)\) is very large, but not extremely — Googology Wiki user {{{2}}} provided a heuristic argument for \(\text{BH}(3) < f_{\varepsilon_0}(n)\) for some reasonably small \(n\).Modèle:Citation needed
The Buchholz hydra surpasses TREE(n) and SCG(n). It is likely weaker than loader.c as well as numbers from finite promise games.
Analysis
It is possible to make one-to-one correspondence between some hydras and ordinals.
To convert a tree or subtree to an ordinal:
- Inductively convert all the immediate children of the node to ordinals.
- Add up those child ordinals. If there were no children, this will be 0.
- If the label of the node is not +, apply \(\psi_\alpha\), where \(\alpha\) is the label of the node, and \(\psi\) is Buchholz's function.
The resulting ordinal expression is only useful if it is in normal form.
Some examples are:
| Hydra | Ordinal |
|---|---|
| (+) | 0 |
| (+(0)) | \(\psi_0(0) = 1\) |
| (+(0)(0)) | \(\psi_0(0) + \psi_0(0) = 2\) |
| (+(0(0))) | \(\psi_0(\psi_0(0)) = \omega\) |
| (+(0(0))(0)) | \(\psi_0(\psi_0(0)) + \psi_0(0) = \omega + 1\) |
| (+(0(0))(0(0))) | \(\psi_0(\psi_0(0)) + \psi_0(\psi_0(0)) = \omega 2\) |
| (+(0(0)(0))) | \(\psi_0(\psi_0(0) + \psi_0(0)) = \omega^2\) |
| (+(0(0(0)))) | \(\psi_0(\psi_0(\psi_0(0))) = \omega^\omega\) |
| (+(0(1))) | \(\psi_0(\psi_1(0)) = \varepsilon_0\) |
| (+(0(1)(1))) | \(\psi_0(\psi_1(0) + \psi_1(0)) = \varepsilon_1\) |
| (+(0(1(0)))) | \(\psi_0(\psi_1(\psi_0(0))) = \varepsilon_\omega\) |
| (+(0(1(1)))) | \(\psi_0(\psi_1(\psi_1(0))) = \zeta_0\) |
| (+(0(1(1(1))))) | \(\psi_0(\psi_1(\psi_1(\psi_1(0)))) = \Gamma_0\) |
| (+(0(1(1(1(0)))))) | \(\psi_0(\psi_1(\psi_1(\psi_1(\psi_0(0))))) = \)SVO |
| (+(0(1(1(1(1)))))) | \(\psi_0(\psi_1(\psi_1(\psi_1(\psi_1(0))))) = \)LVO |
| (+(0(2))) | \(\psi_0(\psi_2(0)) = \)BHO |
| (+(0(\(\omega\)))) | \(\psi_0(\psi_\omega(0))\) |
Sources and References
- W. Buchholz, An independence result for (Π11 - CA) + BI, Ann. Pure Appl. Logic 33 (1987) 131-155.
- 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.