Buchholz hydra

The Buchholz hydraW. Buchholz, An independence result for (Π11 - CA) + BI, Ann. Pure Appl. Logic 33 (1987) 131-155., defined by Wilfried Buchholz in 1987, is a finite tree extended from Kirby-Paris hydra.L. Kirby, J. Paris, Accessible independence results for Peano Arithmetic, Bull. Lon. Math. Soc. 14 (1982) 285-293. The game with the Buchholz hydra is referred as Buchholz's Hydra Game.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. Exact rule of the game is not written in the original paper of Buchholz and the interpretation of the rule of the game may differ among scholars.
This article describes a version of the Buchholz hydra game.Buchholz (1987) just refers to a single step to cut an arbitrary node and a restricted game which only allows steps to cut the rightmost node. Hamano and Okada (1997) define their "Buchholz hydra game" with slight modification of Buchholz (1987), implying that Hamano and Okada acknowledged a certain rule of original Buchholz hydra game. Therefore, canonical definition of the original Buchholz hydra game may be vague to some extent. The rule of the game described in this article is based on the interpretation of LittlePeng9 who originally wrote this article. It is a one-player game played on trees labelled with any finite number or \(\omega\). Then some results with the hydra game are shown, including a fast-growing function \(\text{BH}(n)\) which is relevant to googology.
==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, Hercules chooses 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\). 
# (See illustration) 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. Following terminology in some papers, we use the term strategy as meaning the sequence of picking leaves. A strategy is a winning strategy if it eventually leaves us with only the root node, and a losing strategy otherwise.
== Results ==
=== Theorems ===
Buchholz proved following Theorems (in a sufficiently strong meta theory which proves the consistency of \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) so that the unprovability in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) works):
* Theorem I: By always chopping off the rightmost head, Hercules is able to kill every hydra in a finite number of steps.
* Theorem II: For every fixed hydra A, Theorem I is provable in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).
* Theorem III: Suppose we make a tree with just one branch with \(x\) nodes, labeled \(+,0,\omega,\omega,...,\omega\). Call such a tree \(R^x\). Then it cannot 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\).)
===\(\text{BH}(n)\) function===
\(\text{BH}(n)\) is a fast-growing function defined by a Googology wiki user Wojowu or on 10 April 2013.The first version of this article by LittlePeng9 on 10 April 2013
Define \(\text{BH}(x)\) as the smallest \(k\) such that \(R^x(1)(2)(3)...(k)\) as defined in #Theorems is root tree. By Theorem I this function is total on \(\mathbb{N}\) in the meta theory, but by Theorem III the meta theory proves that (the formalisation of) its totality cannot be proven in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).
Then for example,
* \(\text{BH}(1) = 0\) because \(R^1\) is a root tree by definition.
* \(\text{BH}(2) = 1\) because \(R^2\) is a tree with 2 nodes labeled +,0, and therefore \(R^2(1)\) is a root tree.
* \(\text{BH}(3)\) is very large, but not extremely for googologists — Googology Wiki user provided a heuristic argument for \(\text{BH}(3) < f_{\varepsilon_0}(n)\) for some reasonably small \(n\).User_blog:Wythagoras/Upper_bound_on_the_Buchholz_hydra
Some statements about the growth rate of \(\text{BH}(n)\) function were described in this article without proof. They are listed at #Growth rate of BH(n) function.
=== Correspondence to ordinal ===
It is possible to make one-to-one correspondence between some hydras and ordinals by composing \(|\cdot|\) and the canonical map \(o \colon OT \to \textrm{On}\) for Buchholz's function.
If we restrict it to the subset of subtrees corresponding to normal forms for \(OT\), the conversion can be described in the following way:
# 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 conversion itself works for subtrees which do not necessarily correspond to normal forms, but the resulting ordinal expression is not necessarily compatible with the structure of the game.
Some examples are (Note: Rule of the notation of the hydra in this table is undocumented.This notation system of Buchholz hydra seems to have been used in this community since 2013, for example in Vel's post on April 16, 2013 but source of the notation and exact documentation of the notation system is not known. Adding explanation with source to the article is appreciated. See also talk page.):
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))\)
== History of discussion ==
=== Growth rate of BH(n) function ===
Some statements about the growth rate of \(\text{BH}(n)\) function were described in this article without proof. Such descriptions, which might be wrong due to the lack of proofs, are listed here.
* In the first version of this article, described that the growth rate of BH(n) is "comparable to \(f_{\psi_0(\varepsilon_{\Omega_\omega + 1})}(n)\)" with respect to unspecified system of fundamental sequences. Here \(\psi\) denotes Buchholz's function, and \(\psi_0(\varepsilon_{\Omega_\omega + 1})\) is the Takeuti-Feferman-Buchholz ordinal, which measures the strength of \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).Buchholz, Feferman, Pohlers, and Sieg, Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics, Vol. 897 (1981), Springer-Verlag Berlin Heidelberg.
* Googology wiki user describedVel!'s edit on 26 March 2015 that \(\text{BH}(n)\) eventually dominates all recursive functions provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).The statement impies that \(\text{BH}(n)\) itself is total in an unspecified meta theory in which the provability in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) is argued, but is not provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) with respect to any formalisation in arithmetic.
* Vel! described that \(\text{BH}(n)\) is provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) + "the TFB ordinal is well-ordered". rewrote the sentenceP進大好きbot's edit on 5 January 2020 to "\(\text{BH}(n)\) is itself provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) + "transfinite induction with respect to TFB"."
* It was described that \(\text{BH}(n)\) surpasses TREE(n) and SCG(n).It is very difficult to analyse these two functions, and hence there are many unsourced analyses of them in this wiki. For more details, see TREE sequence#Issues on other analyses.
* It was described that \(\text{BH}(n)\) is likely weaker than loader.c as well as numbers from finite promise games.
=== Hydra theorem ===
It was described in the old version of this wiki that there are no losing strategies for any hydra. Call this statement the hydra theorem. Wilfried Buchholz was cited for showing this, but the source of this article does not include such a result. A similar description is found in Kirby-Paris hydra#Hydra Theorem.
== See also ==
* Papers which may be related to Buchholz hydra
* Papers which cite Buchholz (1987)
* Blog posts about Buchholz hydra
== Footnotes ==
== References ==
ja:ブーフホルツのヒドラ
fr:Hydre de Buchholz
Category:Functions
Category:Games