- Not to be confused with Buchholz's function.
- See also: Kirby-Paris hydra
The Buchholz hydra[1], defined by Wilfried Buchholz in 1987, is a finite tree extended from Kirby-Paris hydra.[2] The game with the Buchholz hydra is referred as Buchholz's Hydra Game.[3][4][note 1]
This article describes a version of the Buchholz hydra game.[note 2] 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,[2][3] 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):[1]
- 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 LittlePeng9 on 10 April 2013.[5]
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 Wythagoras provided a heuristic argument for \(\text{BH}(3) < f_{\varepsilon_0}(n)\) for some reasonably small \(n\).[6]
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.[note 3]):
| 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, LittlePeng9 described[5] 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}\).[7][note 4]
- Googology wiki user Vel! described[9] that \(\text{BH}(n)\) eventually dominates all recursive functions provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).[note 5]
- Vel! described[9] that \(\text{BH}(n)\) is provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) + "the TFB ordinal is well-ordered". P進大好きbot rewrote the sentence[10] to "\(\text{BH}(n)\) is itself provably total in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) + "transfinite induction with respect to TFB"."[note 6]
- It was described that \(\text{BH}(n)\) surpasses TREE(n) and SCG(n).[note 7]
- It was described that \(\text{BH}(n)\) is likely weaker than loader.c[note 8] 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.[note 9] 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[]
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ In the talk page of subcubic graph number, there was a discussion about comparison of SCG function and BH function,[8] where BH(n) function, described as BHydra(n) here, is mentioned and the growth rate is discussed. The description of this article appears to be based on such discussion in this community. However, such a comparison does not make sense unless we fix a specific system of fundamental sequences. Note that there was a common misconception that the growth rate of the fast-growing hierarchy does not depend on a choice of a system of fundamental sequence, and hence the lack of the choice might be based on this misconception.
- ↑ 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.
- ↑ The revision is done because the original axiom does not make sense if we actually work in arithmetic, in which TFB does not make sense, and because it has no effect even when we replace the arithmetic to a set theory so that TFB make sense due to the fact that TFB is always well-founded by definition. The alternative axiom was given under the assumption that the original axiom is based on a typical confusion between transfinite induction in some sense along a specific ordinal notation up to TFB and the well-foundedness of TFB itself. P進大好きbot clarified that citation is lacked,[11][12] and hence the revision does not mean that there is a proof for the alternative statement.
- ↑ 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.
- ↑ Since it is difficult to understand the definition of loader.c, there are many unsourced statements on loader.c in this wiki.[13] For example, the article says that loader's number is much bigger than \(\text{BH}(100)\),[13] but there is no actual proof or source written in the article.
- ↑ What Buchholz showed is the canonical correspondence \(|\cdot|\)[1] p. 136 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,[1] 2.1 Theorem (b) 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\)). He neither states nor implies the hydra theorem. Instead, he only referred to the fact that the sequence of the rightmost leaves is a winning strategy.[1] Theorem I A statement weaker than the hydra theorem is unprovable in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).[1] Theorem I It is unknown if it is provable for individual hydras, although it was described in the old version of this wiki that it is provable.
References[]
- ↑ 1.0 1.1 1.2 1.3 1.4 1.5 W. Buchholz, An independence result for (Π11 - CA) + BI, Ann. Pure Appl. Logic 33 (1987) 131-155.
- ↑ 2.0 2.1 L. Kirby, J. Paris, Accessible independence results for Peano Arithmetic, Bull. Lon. Math. Soc. 14 (1982) 285-293. doi:10.1112/blms/14.4.285
- ↑ 3.0 3.1 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. doi:10.1002/malq.19970430113
- ↑ M. Hamano, M. Okada, A direct independence proof of Buchholz's Hydra Game on finite labeled trees, Arch. Math. Logic 37 (1998) 67-89. doi:10.1007/s001530050084
- ↑ 5.0 5.1 The first version of this article by LittlePeng9 on 10 April 2013
- ↑ User_blog:Wythagoras/Upper_bound_on_the_Buchholz_hydra
- ↑ 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.
- ↑ Talk:Subcubic graph number#Actual strength of SCG function (See Deedlit11's post on March 8, 2013 and LittlePeng9's post on March 9, 2013)
- ↑ 9.0 9.1 Vel!'s edit on 26 March 2015
- ↑ P進大好きbot's edit on 5 January 2020
- ↑ p進大好きbot's edit on 2 October 2021
- ↑ p進大好きbot's edit on 2 October 2021
- ↑ 13.0 13.1 The version of the article of loader.c retrieved at 4 November 2021.