Buchholz hydra

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 mathematical tree. The hydra game can be used to generate a rapidly growing function, ${\displaystyle BH(n)}$, which eventually dominates all recursive functions that are provably total in "${\displaystyle {\textrm {ID}}_{\nu }}$", and the termination of all hydra games is not provably total in ${\displaystyle {\textrm {(}}\Pi _{1}^{1}{\textrm {-CA)+BI}}}$. ^[1]

Rules

The game is played on a hydra, a finite, rooted connected tree ${\displaystyle A}$, with the following properties:

• The root of ${\displaystyle A}$ has a special label, usually denoted ${\displaystyle +}$.
• Any other node of ${\displaystyle A}$ has a label ${\displaystyle \nu \leq \omega }$.
• All nodes directly above the root of ${\displaystyle A}$ have a label ${\displaystyle 0}$.

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

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

If ${\displaystyle \sigma }$ is the rightmost head of ${\displaystyle A}$, ${\displaystyle A(n)}$ 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. ^[1]

Hydra theorem

Buchholz's paper in 1987 showed that the canonical correspondence between a hydra and an infinitary well-founded tree (or the corresponding term in the notation system ${\displaystyle T}$ associated to Buchholz's function, which does not necessarily belong to the ordinal notation system ${\displaystyle OT\subset T}$), preserves fundamental sequences of choosing the rightmost leaves and the ${\displaystyle (n)}$ operation on an infinitary well-founded tree or the ${\displaystyle [n]}$ operation on the corresponding term in ${\displaystyle T}$. ^[1]

The hydra theorem for Buchholz hydra, stating that there are no losing strategies for any hydra, is unprovable in ${\displaystyle {\mathsf {\Pi _{1}^{1}-CA+BI}}}$. ^[2]

BH(n)

Suppose a tree consists of just one branch with ${\displaystyle x}$ nodes, labelled ${\displaystyle +,0,\omega ,...,\omega }$. Call such a tree ${\displaystyle R^{n}}$. It cannot be proven in ${\displaystyle {\mathsf {\Pi _{1}^{1}-CA+BI}}}$ that for all ${\displaystyle x}$, there exists ${\displaystyle k}$ such that ${\displaystyle R_{x}(1)(2)(3)...(k)}$ is a winning strategy. (The latter expression means taking the tree ${\displaystyle R_{x}}$, then transforming it with ${\displaystyle n=1}$, then ${\displaystyle n=2}$, then ${\displaystyle n=3}$, etc. up to ${\displaystyle n=k}$.) ^[2]

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

The first two values of the BH function are virtually degenerate: ${\displaystyle BH(1)=0}$ and ${\displaystyle BH(2)=1}$. Similarly to the weak tree function, ${\displaystyle BH(3)}$ is very large, but less so.^{[ citation needed ]}

The Buchholz hydra eventually surpasses TREE(n) and SCG(n),^{[ citation needed ]} yet it is likely weaker than loader as well as numbers from finite promise games.

Analysis

It is possible to make a 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 ${\displaystyle \psi _{\alpha }}$, where ${\displaystyle \alpha }$ is the label of the node, and ${\displaystyle \psi }$ is Buchholz's function.

The resulting ordinal expression is only useful if it is in normal form. Some examples are:

Conversion

Hydra	Ordinal
${\displaystyle +}$	${\displaystyle 0}$
${\displaystyle +(0)}$	${\displaystyle \psi _{0}(0)=1}$
${\displaystyle +(0)(0)}$	${\displaystyle 2}$
${\displaystyle +(0(0))}$	${\displaystyle \psi _{0}(1)=\omega }$
${\displaystyle +(0(0))(0)}$	${\displaystyle \omega +1}$
${\displaystyle +(0(0))(0(0))}$	${\displaystyle \omega \cdot 2}$
${\displaystyle +(0(0)(0))}$	${\displaystyle \omega ^{2}}$
${\displaystyle +(0(0(0)))}$	${\displaystyle \omega ^{\omega }}$
${\displaystyle +(0(1))}$	${\displaystyle \varepsilon _{0}}$
${\displaystyle +(0(1)(1))}$	${\displaystyle \varepsilon _{1}}$
${\displaystyle +(0(1(0)))}$	${\displaystyle \varepsilon _{\omega }}$
${\displaystyle +(0(1(1)))}$	${\displaystyle \zeta _{0}}$
${\displaystyle +(0(1(1(1))))}$	${\displaystyle \Gamma _{0}}$
${\displaystyle +(0(1(1(1(0)))))}$	SVO
${\displaystyle +(0(1(1(1(1)))))}$	LVO
${\displaystyle +(0(2))}$	BHO
${\displaystyle +(0(\omega ))}$	BO

References

1. Buchholz, Wilfried (1987), "An independence result for ${\displaystyle (\Pi _{1}^{1}{\text{-CA}})+{\text{BI}}}$", Annals of Pure and Applied Logic, 33 (2): 131–155, doi:10.1016/0168-0072(87)90078-9, MR   0874022
2. Hamano, Masahiro; Okada, Mitsuhiro (1997), "A direct independence proof of Buchholz's Hydra game on finite labeled trees", Archive for Mathematical Logic, 37 (2): 67–89, doi:10.1007/s001530050084, MR   1620664

Further reading

• Hamano, Masahiro; Okada, Mitsuhiro (1997), "A relationship among Gentzen's proof-reduction, Kirby–Paris' hydra game and Buchholz's hydra game", Mathematical Logic Quarterly, 43 (1): 103–120, doi:10.1002/malq.19970430113, MR   1429324
• Gordeev, Lev (December 2001), "Review of 'A direct independence proof of Buchholz's Hydra game on finite labeled trees'", Bulletin of Symbolic Logic, 7 (4): 534–535, doi:10.2307/2687805, ISSN   1079-8986, JSTOR   2687805
• Kirby, Laurie; Paris, Jeff (1982), "Accessible independence results for Peano Arithmetic" (PDF), Bull. London Math. Soc., 14 (4): 285–293, doi:10.1112/blms/14.4.285 , retrieved 2021-09-03
• Ketonen, Jussi; Solovay, Robert (1981), "Rapidly growing Ramsey functions", Annals of Mathematics, 113 (2): 267–314, doi:10.2307/2006985, ISSN   0003-486X, JSTOR   2006985 , retrieved 2021-09-03
• Takeuti, Gaisi (2013), Proof theory (2nd edition (reprint) ed.), Newburyport: Dover Publications, ISBN   978-0-486-32067-0, OCLC   1162507470

External links

• "Hydras", Agnijo's mathematical treasure chest, retrieved 2021-09-04

 This article incorporates text available under the CC BY-SA 3.0 license.