View source for Buchholz hydra

{{short description|Hydra game in mathematical logic}}
In [[mathematics]], especially [[mathematical logic]], [[graph theory]] and [[number theory]], the '''Buchholz hydra game''' is a type of [[hydra game]], which is a single-player game based on the idea of chopping pieces off a [[Tree (graph theory)|mathematical tree]]. The hydra game can be used to generate a rapidly growing [[Function (mathematics)|function]], <math>BH(n)</math>, which eventually dominates all [[Computable function|recursive functions]] that are provably [[total function|total]] in "<math>\textrm{ID}_{\nu}</math>", and the termination of all hydra games is not provably total in <math>\textrm{(}\Pi_1^1\textrm{-CA)+BI}</math>.{{r|buchholz}}

==Rules==
The game is played on a ''hydra'', a finite, [[Rooted graph|rooted]] [[Connectivity (graph theory)|connected]] [[Tree (graph theory)|tree]] <math>A</math>, with the following properties:

* The root of <math>A</math> has a special label, usually denoted <math>+</math>.
* Any other node of <math>A</math> has a label <math>\nu \leq \omega</math>.
* All nodes directly above the root of <math>A</math> have a label <math>0</math>.

If the player decides to remove the top node <math>\sigma</math> of <math>A</math>, the hydra will then choose an arbitrary <math>n \in \N</math>, where <math>n</math> is a current turn number, and then transform itself into a new hydra <math>A(\sigma, n)</math> as follows. Let <math>\tau</math> represent the parent of <math>\sigma</math>, and let <math>A^-</math> represent the part of the hydra which remains after <math>\sigma</math> has been removed. The definition of <math>A(\sigma, n)</math> depends on the label of <math>\sigma</math>:

* If the label of <math>\sigma</math> is 0 and <math>\tau</math> is the root of <math>A</math>, then <math>A(\sigma, n)</math> = <math>A^-</math>.
* If the label of <math>\sigma</math> is 0 but <math>\tau</math> is not the root of <math>A</math>, <math>n</math> copies of <math>\tau</math> and all its children are made, and edges between them and <math>\tau</math>'s parent are added. This new tree is <math>A(\sigma, n)</math>.
* If the label of <math>\sigma</math> is <math>u</math> for some <math>u \in \N</math>, let <math>\varepsilon</math> be the first node below <math>\sigma</math> that has a label <math>v < u</math>. Define <math>B</math> as the subtree obtained by starting with <math>A_\varepsilon</math> and replacing the label of <math>\varepsilon</math> with <math>u - 1</math> and <math>\sigma</math> with 0. <math>A(\sigma, n)</math> is then obtained by taking <math>A</math> and replacing <math>\sigma</math> with <math>B</math>. In this case, the value of <math>n</math> does not matter.
* If the label of <math>\sigma</math> is <math>\omega</math>, <math>A(\sigma, n)</math> is obtained by replacing the label of <math>\sigma</math> with <math>n + 1</math>.

If <math>\sigma</math> is the rightmost head of <math>A</math>, <math>A(n)</math> is written. A series of moves is called a strategy. A strategy is called a winning strategy if, after a finite amount of moves, the hydra reduces to its root. This always terminates, even though the hydra can get taller by massive amounts.{{r|buchholz}}

==Hydra theorem==
Buchholz's paper in 1987 showed that the canonical correspondence between a hydra and an [[Infinitary logic|infinitary]] well-founded tree (or the corresponding term in the notation system <math>T</math> associated to Buchholz's function, which does not necessarily belong to the ordinal notation system <math>OT \subset T</math>), preserves fundamental sequences of choosing the rightmost leaves and the <math>(n)</math> operation on an infinitary well-founded tree or the <math>[n]</math> operation on the corresponding term in <math>T</math>.{{r|buchholz}}

The hydra theorem for Buchholz hydra, stating that there are no losing strategies for any hydra, is unprovable in <math>\mathsf{\Pi^1_1 - CA + BI}</math>.{{r|hamano-okada}}

==BH(n)==
Suppose a tree consists of just one branch with <math>x</math> nodes, labelled <math>+, 0, \omega, ..., \omega</math>. Call such a tree <math>R^n</math>. It cannot be proven in <math>\mathsf{\Pi^1_1 - CA + BI}</math> that for all <math>x</math>, there exists <math>k</math> such that <math>R_x(1)(2)(3)...(k)</math> is a winning strategy. (The latter expression means taking the tree <math>R_x</math>, then transforming it with <math>n=1</math>, then <math>n=2</math>, then <math>n=3</math>, etc. up to <math>n=k</math>.){{r|hamano-okada}}

Define <math>BH(x)</math> as the smallest <math>k</math> such that <math>R_x(1)(2)(3)...(k)</math> as defined above is a winning strategy. By the hydra theorem, this function is well-defined, but its totality cannot be proven in <math>\mathsf{\Pi^1_1 - CA + BI}</math>. Hydras grow extremely fast, because the amount of turns required to kill <math>R_x(1)(2)</math> is larger than [[Graham's number]] or even the amount of turns to kill a Kirby-Paris hydra; and <math>R_x(1)(2)(3)(4)(5)(6)</math> has an entire Kirby-Paris hydra as its branch. To be precise, its rate of growth is believed to be comparable to <math>f_{\psi_0(\varepsilon_{\Omega_\omega + 1})}(x)</math> with respect to the unspecified system of fundamental sequences without a proof. Here, <math>\psi_0</math> denotes Buchholz's function, and <math>\psi_0(\varepsilon_{\Omega_\omega + 1})</math> is the [[Takeuti-Feferman-Buchholz ordinal]] which measures the strength of <math>\mathsf{\Pi^1_1 - CA + BI}</math>.

The first two values of the BH function are virtually degenerate: <math>BH(1) = 0</math> and <math>BH(2) = 1</math>. Similarly to the weak tree function, <math>BH(3)</math> is very large, but less so.{{fact|date=September 2021}}

The Buchholz hydra eventually surpasses TREE(n) and [[Friedman's SSCG function|SCG(n)]],{{Citation needed|date=November 2021}} yet it is likely weaker than loader as well as numbers from finite promise games.

==Analysis==
{{Uncited section|date=January 2023}}

It is possible to make a one-to-one correspondence between some hydras and [[Ordinal number|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 <math>\psi_\alpha</math>, where <math>\alpha</math> is the label of the node, and <math>\psi</math> is Buchholz's function.

The resulting ordinal expression is only useful if it is in normal form. Some examples are:
{| class="wikitable"
|+Conversion
!Hydra
!Ordinal
|-
|<math>+</math>
|<math>0</math>
|-
|<math>+(0)</math>
|<math>\psi_0(0) = 1</math>
|-
|<math>+(0)(0)</math>
|<math>2</math>
|-
|<math>+(0(0))</math>
|<math>\psi_0(1) = \omega</math>
|-
|<math>+(0(0))(0)</math>
|<math>\omega + 1</math>
|-
|<math>+(0(0))(0(0))</math>
|<math>\omega \cdot 2</math>
|-
|<math>+(0(0)(0))</math>
|<math>\omega^2</math>
|-
|<math>+(0(0(0)))</math>
|<math>\omega^\omega</math>
|-
|<math>+(0(1))</math>
|<math>\varepsilon_0</math>
|-
|<math>+(0(1)(1))</math>
|<math>\varepsilon_1</math>
|-
|<math>+(0(1(0)))</math>
|<math>\varepsilon_\omega</math>
|-
|<math>+(0(1(1)))</math>
|<math>\zeta_0</math>
|-
|<math>+(0(1(1(1))))</math>
|<math>\Gamma_0</math>
|-
|<math>+(0(1(1(1(0)))))</math>
|[[Small Veblen ordinal|SVO]]
|-
|<math>+(0(1(1(1(1)))))</math>
|[[Large Veblen ordinal|LVO]]
|-
|<math>+(0(2))</math>
|[[Bachmann–Howard ordinal|BHO]]
|-
|<math>+(0(\omega))</math>
|[[Buchholz's ordinal|BO]]
|}

==References==
{{Reflist | refs = 
<ref name=buchholz>{{citation
 | last = Buchholz | first = Wilfried
 | doi = 10.1016/0168-0072(87)90078-9
 | issue = 2
 | journal = Annals of Pure and Applied Logic
 | mr = 874022
 | pages = 131–155
 | title = An independence result for <math>(\Pi^1_1\text{-CA})+\text{BI}</math>
 | volume = 33
 | year = 1987}}</ref>

<ref name=hamano-okada>{{citation
 | last1 = Hamano | first1 = Masahiro
 | last2 = Okada | first2 = Mitsuhiro
 | doi = 10.1007/s001530050084
 | issue = 2
 | journal = Archive for Mathematical Logic
 | mr = 1620664
 | pages = 67–89
 | title = A direct independence proof of Buchholz's Hydra game on finite labeled trees
 | volume = 37
 | year = 1997}}</ref>

}}

==Further reading==
{{refbegin}}
*{{citation
 | last1 = Hamano | first1 = Masahiro
 | last2 = Okada | first2 = Mitsuhiro
 | doi = 10.1002/malq.19970430113
 | issue = 1
 | journal = Mathematical Logic Quarterly
 | mr = 1429324
 | pages = 103–120
 | title = A relationship among Gentzen's proof-reduction, Kirby–Paris' hydra game and Buchholz's hydra game
 | volume = 43
 | year = 1997}}
*{{citation|last1=Gordeev|first1=Lev|date=December 2001|title=Review of 'A direct independence proof of Buchholz's Hydra game on finite labeled trees'|journal=Bulletin of Symbolic Logic|volume=7|issue=4|pages=534–535|doi=10.2307/2687805|jstor=2687805|issn=1079-8986}}
* {{citation|last1=Kirby|first1=Laurie|title=Accessible independence results for Peano Arithmetic|url=https://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf|access-date=2021-09-03|last2=Paris|first2=Jeff|journal=Bull. London Math. Soc.|volume=14|year=1982|issue=4|pages=285–293|doi=10.1112/blms/14.4.285}}
*{{citation|last1=Ketonen|first1=Jussi|last2=Solovay|first2=Robert|date=1981|title=Rapidly growing Ramsey functions|url=https://www.jstor.org/stable/2006985|journal=Annals of Mathematics|volume=113|issue=2|pages=267–314|doi=10.2307/2006985|jstor=2006985|issn=0003-486X|access-date=2021-09-03}}
*{{citation|last1=Takeuti|first1=Gaisi|title=Proof theory|edition=2nd edition (reprint)|date=2013|publisher=Dover Publications|isbn=978-0-486-32067-0|location=Newburyport|oclc=1162507470}}
{{refend}}

==External links==
*{{citation|url=http://agnijomaths.com/categories/number_theory/abstract_number_theory/hydras.html|title=Hydras|website=Agnijo's mathematical treasure chest|access-date=2021-09-04}}

{{cc-notice|cc=bysa3|url=https://googology.wikia.org/wiki/Buchholz_hydra}}

{{Large numbers}}

[[Category:Trees (graph theory)]]
[[Category:Mathematical games]]
[[Category:Large numbers]]
[[Category:Ordinal numbers]]
[[Category:Theorems in discrete mathematics]]