Buchholz hydra

Summary

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, $BH(n)$, which eventually dominates all recursive functions that are provably total in "$\textrm{ID}_{\nu}$", and it is not provable that all hydra games terminate in $\textrm{(}\Pi_1^1\textrm{-CA)+BI}$.