Not to be confused with Buchholz's function.
See also: Kirby-Paris hydra

The Buchholz hydra game is a one-player game played on trees labelled with any finite number or \(\omega\). From the game arises a fast-growing function \(\text{BH}(n)\) which eventually dominates all recursive functions provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\), and is itself provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) + "transfinite induction with respect to TFB".


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 perform a transformation on the tree with two parameters: a leaf node \(a\) and a nonnegative integer \(n\). We alter the hydra using the following rules:

  1. 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\).
  2. 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'\).
  3. 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 and values of \(n\). The sequence of leaves and \(n\)'s 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.

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 cannot[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 Wythagoras provided a heuristic argument for \(\text{BH}(3) < f_{\varepsilon_0}(n)\) for some reasonably small \(n\).[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.


It is possible to make one-to-one correspondence between some hydras and ordinals.

To convert a tree or subtree to an ordinal:

  1. Inductively convert all the immediate children of the node to ordinals.
  2. Add up those child ordinals. If there were no children, this will be 0.
  3. 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

  • 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.
Community content is available under CC-BY-SA unless otherwise noted.