Buchholz hydra

Summary

(Learn how and when to remove this template message)

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 the termination of all hydra games is not provably total in .[1]

Rules edit

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. 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[citation needed], even though the hydra can get taller by massive amounts.

Hydra theorem edit

Buchholz's paper in 1987[2] 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  .[3]

BH(n) edit

Suppose a tree consists of just one branch with   nodes, labelled  . Call such a tree  . It cannot[citation needed] 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.[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 edit

It is possible to make a one-to-one correspondence between some hydras and ordinals[citation needed]. 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:

Conversion
Hydra Ordinal
   
   
   
   
   
   
   
   
   
   
   
   
   
  SVO
  LVO
  BHO
  BO

References edit

  1. ^ W. Buchholz, "An independence result for (Π1
    1
    -CA)+BI Archived 2023-05-09 at the Wayback Machine" (1987), Annals of Pure and Applied Logic vol. 33, pp.131--155
  2. ^ Buchholz, Wilfried (1987). "An independence result for (Π1
    1
    -CA)+BI". Annals of Pure and Applied Logic. 33: 131–155. doi:10.1016/0168-0072(87)90078-9.
  3. ^ Hamano, Masahiro; Okada, Mitsuhiro (1998-03-01). "A direct independence proof of Buchholz's Hydra Game on finite labelled trees". Archive for Mathematical Logic. 37 (2): 67–89. doi:10.1007/s001530050084. ISSN 0933-5846. S2CID 40113368. Archived from the original on 2023-08-13. Retrieved 2022-05-22.
  • Buchholz, Wilfried (1987). "An independence result for (Π11 - CA) + BI" (PDF). Annals of Pure and Applied Logic. 33. North-Holland: 131–155. doi:10.1016/0168-0072(87)90078-9. Retrieved 2021-09-03.
  • Hamano, Masahiro; Okada, Mitsuhiro (1995). "A relationship among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game (Preliminary Report)" (PDF). Research Institute for Mathematical Sciences. 912: 64–81. Retrieved 2021-09-03.
  • 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. ISSN 0942-5616. S2CID 26893598.
  • Hamano, Masahiro; Okada, Mitsuhiro (1998-03-01). "A direct independence proof of Buchholz's Hydra Game on finite labelled trees". Archive for Mathematical Logic. 37 (2): 67–89. doi:10.1007/s001530050084. ISSN 0933-5846. S2CID 40113368.
  • Gordeev, Lev (December 2001). "(Review) Masahiro Hamano and Mitsuhiro Okada. A direct independence proof of Buchholz's Hydra game on finite labelled trees. Archive for mathematical logic, vol. 37 no. 2 (1998), pp. 67–89". 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.
  • "Hydras". Agnijo's mathematical treasure chest. Retrieved 2021-09-04.

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