- 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".[citation needed]
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 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.
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))\) |
Komi Amiko's Extension (Amiko hydras) (Citation needed)
A natural question to ask when investigating ways to build faster growing functions than the one based on Buchholz hydras is "what if we used higher ordinals as labels?" Then, because hydras are ordinal-like, "what if we used nested hydras as labels?" We can ignore the details of adapting ordinal transformation rules for hydras for the time being, but these nested hydras are unquestionably more powerful than plain Buchholz hydras.
He then added a singleton, which he refers to as \(\lambda\). When encountered, it would expand into a hydra involving labels that are hydras involving labels that are hydras involving labels that are hydras... \(N\) layers deep, despite the absence of any mention of \(\lambda\). In some ways, this is a fixed point ordinal of hydra nesting, or, more precisely, the first common fixed point of whatever ordinal operation nesting hydras corresponds to. I'm not sure what ordinal such a system corresponds to, but it's certainly stronger than without \(\lambda\). Why should we stop there? We can rename \(\lambda\) to \(\lambda_0\) and then introduce \(\lambda_1\), the second common fixed point of hydra nesting, which expands similarly to \(\lambda_0\) but contains \(\lambda_0\) in the nested hydras.
Why should we stop there? Subscript ordinals, and even hydra subscripts can be created. Then we can add another layer, say, \(\zeta_0\), which expands into a stack of nested \(\lambda\) hydras, and so on.
“Externalize” and “close” are two important basic transformation types in our toolbox of higher order hydra construction transformations. The term "externalise" refers to the process of shifting information from the labels (internal) to the children (external), with the ultimate goal of putting an upper bound on the labels without affecting the strength of the construction. “Close” means to take a construction with upper-bounded labels and extend it to support arbitrary hydras as labels, thereby taking the closure of the construction under using hydras as labels and making the construction stronger. These two go together like clockwork. These are called transformation types because there isn't just one way to externalise or close, and the strength of different possible transformations can vary.
Amiko hydras can be made from Buchholz hydras by taking a close step, a somewhat strong externalise step, and then another close step. The externalise step is the most intriguing here. Below is a comparison between the initial Buchholz hydra and its Amiko equivalent:
The initial state of the Buchholz hydra.
The final state of the Amiko hydra.
That's it, our first Amiko hydra! Whatever rules we use to define its evolution, it should evolve similarly to Buchholz hydras for hydras converted from Buchholz hydras.
Amiko hydras with only \(0 = (+:)\) and \(1 = (+:((+:):))\) labels correspond to nested Buchholz hydras. Amiko hydras with finite labels correspond to hyper-nested Buchholz hydras with a finite number of hyper-nesting dimensions, which we may collectively call \(\textrm{hyper}^\omega\)-nested Buchholz hydras. The full construction of Amiko hydras, obtained by applying a close transform after this externalize, is far more powerful, and its corresponding ordinal is the first common fixed point of “\(\alpha\) maps to the ordinal of \(\textrm{hyper}^\alpha\)-nested Buchholz hydras.”
It’s useful to be able to show a Buchholz hydra can be converted into an equivalent Amiko hydra, since it shows that Amiko hydras are at least as strong as Buchholz hydras.
The root just becomes a root node. All its children are then recursively transformed with this procedure:
"Recursively transform its children. Let \(\alpha\) be the label of the Buchholz hydra node. Change its label to \((+:)\). If \(\alpha\) is finite, then insert \(\alpha\) copies of \(((+:((+:):)):)\) just before its leftmost child. Otherwise, insert \(((+:((+:):)):((+:):))\) just before its leftmost child."
As you can see, the hydras converted this way are nowhere near the largest Amiko hydras allow. The converted Amiko hydra will not necessarily evolve in the same way as the Buchholz hydra, but they will correspond to the same ordinal and have the same growth rate if analogous fast growing functions are defined on them.
Comparison operators may include a filter, which refers to the labels of the nodes being compared and causes children who do not match the filter to be ignored. In recursive comparisons, the filter does not propagate. Writing \(A<>_{>C}B\), for example, means comparing \(A\) and \(B\) as if all of their immediate children with labels \(\leq C\) were removed.
Let \(S(A)\) be the outer reduction function, which is what we mean by reducing a hydra that includes the root node. It is defined like so:
If we are reducing \(A\), it is guaranteed that it has children. Let \(B\) be \(A\)'s rightmost child, and \(C\) be \(B\)'s label:
- If \(C = (+:)\), search for the rightmost leaf of \(A\), but do not enter nodes with labels \(> (+:)\). Let \(D\) be this rightmost leaf (whose label is guaranteed to be \((+:)\)). Then:
- If \(D\) has no children, let \(E\) be the parent of \(D\). Remove \(D\) from \(E\). If \(E\) has a parent, append \(N\) copies of \(E\) as additional children to the parent of \(E\), for some \(N\). \(S(A)\) is the modified \(A\).
- If \(D\) has any children (all of which are guaranteed to have a label \(> (+:)\)), traverse up the parents of \(D\), searching for a node \(E\) satisfying \(E <_{>(+:)} D\), but do not enter nodes with label \(> (+:)\). If no suitable \(E\) is found, take \(E\) as the last candidate's parent (or \(A\) if it was reached) but with all children removed except the rightmost. Let \(D'\) be \(D\) but with the label changed to \(+\). Let \(E'\) be \(S(D')\) but without children whose label is \((+:)\), and with the children of \(E\) whose labels are \((+:)\) appended, and with label \(D\). Let \(F = ((+:):)\). Then, repeat the following \(N\) times, for some \(N\): replace \(F\) with \(E'\) where \(D\) is replaced with \(F\). Then finally replace \(D\) with \(F\). \(S(A)\) is the modified \(A\).
- If \(C > (+:)\), go right in the tree, looking for the rightmost leaf. If \(C\) has no children, the search just ends there. Otherwise:
- If a node \(D\) with label \((+:)\) is encountered, proceed as in rule 1.
- If we reach a leaf without ever encountering a node with label \((+:)\), let \(D\) be this rightmost leaf, and let \(E\) be \(D\)'s label. Traverse up the parents of \(D\) searching for a node \(F\) with label \(G\) satisfying \(G < E\), which is always guaranteed to exist. Let \(H = S(E)\). Let \(F'\) be \(F\) but with the label changed to \(H\), and let \(I = ((+:):)\). Then, repeat the following \(N\) times, for some \(N\): replace \(I\) with \(F'\) where \(D\) is replaced with \(I\). Then finally replace \(D\) with \(I\). \(S(A)\) is the modified \(A\).
He then defined a fast-growing function \(AH(k)\) like so:
Begin with the smallest possible hydra, which is \((+:)\). Then repeat \(k\) times: \(A \mapsto (+:(A:))\). Begin with a global shared counter \(N\), which will increment after every time it is called for (including additional mentions when reducing nested hydras), not on each outer evaluation of \(S\). Reduce the hydra using \(S\) until it is \((+:)\). The final value of \(N\) is \(AH(k)\). The fist few values:
- \(AH(0) = 1\)
- \(AH(1) = 1\)
- \(AH(2) = 3\)
\(AH(3)\) already blows Buchholz hydras (and finitely hyper-nested Buchholz hydras) out of the water!
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.
- K. Amiko, Amiko Hydras, 2020