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, , which eventually dominates all recursive functions that are provably total in "", and it is not provable that all hydra games terminate in .
The game is played on a hydra, a finite, rooted connected tree , with the following properties:
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 is the rightmost head of , 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.
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 .
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 .
It is possible to make a one-to-one correspondence between some hydras and ordinals. To convert a tree or subtree to an ordinal:
The resulting ordinal expression is only useful if it is in normal form. Some examples are: