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 of a mathematical tree. The hydra game can be used to generate a rapidly growing function, , which eventually dominates all recursive functions that are provably total in "", and the termination of all hydra games is not provably total in . Rules 
The game is played on a hydra, a finite, rooted connected tree , with the following properties:

 The root of  has a special label, usually denoted . Any other node of  has a label . All nodes directly above the root of  have a label . If the player decides to remove the top node  of , the hydra will then choose an arbitrary , where  is a current turn number, and then transform itself into a new hydra  as follows. Let  represent the parent of , and let  represent the part of the hydra which remains after  has been removed. The definition of  depends on the label of :

 If the label of  is 0 and  is the root of , then  = . If the label of  is 0 but  is not the root of ,  copies of  and all its children are made, and edges between them and 's parent are added. This new tree is . If the label of  is  for some , then the first node below  is labelled  as . is then the subtree obtained by starting with  and replacing the label of  with  and  with 0.  is then obtained by taking  and replacing  with . In this case, the value of  does not matter. If the label of  is ,  is obtained by replacing the label of  with . If  is the rightmost head of ,  is written. A series of moves is called a strategy, and a strategy is called a winning strategy if, after a finite amount of moves, the hydra reduces to its root. It has been proven that this always terminates, even though the hydra can get taller by massive amounts. 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  associated to Buchholz's function, which does not necessarily belong to the ordinal notation system ), preserves fundamental sequences of choosing the rightmost leaves and the  operation on an infinitary well-founded tree or the  operation on the corresponding term in . The hydra theorem for Buchholz hydra, stating that there are no losing strategies for any hydra, is unprovable in . BH(n) 
Suppose a tree consists of just one branch with  nodes, labelled . Call such a tree . It cannot be proven in  that for all , there exists  such that  is a winning strategy. (The latter expression means taking the tree , then transforming it with , then , then , etc. up to .) Define  as the smallest  such that  as defined above is a winning strategy. By the hydra theorem, this function is well-defined, but its totality cannot be proven in . Hydras grow extremely fast, because the amount of turns required to kill  is larger than Graham's number or even the amount of turns to kill a Kirby-Paris hydra; and  has an entire Kirby-Paris hydra as its branch. To be precise, its rate of growth is believed to be comparable to  with respect to the unspecified system of fundamental sequences without a proof. Here,  denotes Buchholz's function, and  is the Takeuti-Feferman-Buchholz ordinal which measures the strength of . The first two values of the BH function are virtually degenerate:  and . Similarly to the weak tree function,  is very large, but less so. The Buchholz hydra eventually surpasses TREE(n) and SCG(n), 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 , where  is the label of the node, and  is Buchholz's function. The resulting ordinal expression is only useful if it is in normal form. Some examples are:

References 

 
 

 

 



Trees (graph theory)
Mathematical games
Large numbers
Ordinal numbers
Theorems in discrete mathematics