Buchholz hydra#BH(n)

{{short description|Hydra game in mathematical logic}}

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 the termination of all hydra games is not provably total in \textrm{(}\Pi_1^1\textrm{-CA)+BI}.{{r|buchholz}}

Rules

The game is played on a hydra, a finite, rooted connected tree A, with the following properties:

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

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

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

If \sigma is the rightmost head of A, 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.{{r|buchholz}}

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 T associated to Buchholz's function, which does not necessarily belong to the ordinal notation system OT \subset T), preserves fundamental sequences of choosing the rightmost leaves and the (n) operation on an infinitary well-founded tree or the [n] operation on the corresponding term in T.{{r|buchholz}}

The hydra theorem for Buchholz hydra, stating that there are no losing strategies for any hydra, is unprovable in \mathsf{\Pi^1_1 - CA + BI}.{{r|hamano-okada}}

BH(n)

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

Define BH(x) as the smallest k such that 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 \mathsf{\Pi^1_1 - CA + BI}.

Analysis

{{Uncited section|date=January 2023}}

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 \psi_\alpha, where \alpha is the label of the node, and \psi is Buchholz's function.

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

class="wikitable"

|+Conversion

!Hydra

!Ordinal

+

|0

+(0)

|\psi_0(0) = 1

+(0)(0)

|2

+(0(0))

|\psi_0(1) = \omega

+(0(0))(0)

|\omega + 1

+(0(0))(0(0))

|\omega \cdot 2

+(0(0)(0))

|\omega^2

+(0(0(0)))

|\omega^\omega

+(0(1))

|\varepsilon_0

+(0(1)(1))

|\varepsilon_1

+(0(1(0)))

|\varepsilon_\omega

+(0(1(1)))

|\zeta_0

+(0(1(1(1))))

|\Gamma_0

+(0(1(1(1(0)))))

|SVO

+(0(1(1(1(1)))))

|LVO

+(0(2))

|BHO

+(0(\omega))

|BO

References

{{Reflist | refs =

{{citation

| last = Buchholz | first = Wilfried

| doi = 10.1016/0168-0072(87)90078-9

| issue = 2

| journal = Annals of Pure and Applied Logic

| mr = 874022

| pages = 131–155

| title = An independence result for (\Pi^1_1\text{-CA})+\text{BI}

| volume = 33

| year = 1987}}

{{citation

| last1 = Hamano | first1 = Masahiro

| last2 = Okada | first2 = Mitsuhiro

| doi = 10.1007/s001530050084

| issue = 2

| journal = Archive for Mathematical Logic

| mr = 1620664

| pages = 67–89

| title = A direct independence proof of Buchholz's Hydra game on finite labeled trees

| volume = 37

| year = 1997}}

}}

Further reading

{{refbegin}}

  • {{citation

| last1 = Hamano | first1 = Masahiro

| last2 = Okada | first2 = Mitsuhiro

| doi = 10.1002/malq.19970430113

| issue = 1

| journal = Mathematical Logic Quarterly

| mr = 1429324

| pages = 103–120

| title = A relationship among Gentzen's proof-reduction, Kirby–Paris' hydra game and Buchholz's hydra game

| volume = 43

| year = 1997}}

  • {{citation|last1=Gordeev|first1=Lev|date=December 2001|title=Review of 'A direct independence proof of Buchholz's Hydra game on finite labeled trees'|journal=Bulletin of Symbolic Logic|volume=7|issue=4|pages=534–535|doi=10.2307/2687805|jstor=2687805|issn=1079-8986}}
  • {{citation|last1=Kirby|first1=Laurie|title=Accessible independence results for Peano Arithmetic|url=https://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf|access-date=2021-09-03|last2=Paris|first2=Jeff|journal=Bull. London Math. Soc.|volume=14|year=1982|issue=4|pages=285–293|doi=10.1112/blms/14.4.285}}
  • {{citation|last1=Ketonen|first1=Jussi|last2=Solovay|first2=Robert|date=1981|title=Rapidly growing Ramsey functions|url=https://www.jstor.org/stable/2006985|journal=Annals of Mathematics|volume=113|issue=2|pages=267–314|doi=10.2307/2006985|jstor=2006985|issn=0003-486X|access-date=2021-09-03|url-access=subscription}}
  • {{citation|last1=Takeuti|first1=Gaisi|title=Proof theory|edition=2nd edition (reprint)|date=2013|publisher=Dover Publications|isbn=978-0-486-32067-0|location=Newburyport|oclc=1162507470}}

{{refend}}