Hydre de Buchholz

Voir aussi: Hydre de Kirby-Paris

Le jeu de l'hydre de Buchholz est un jeu à un joueur joué sur des arbres étiquetés avec un nombre fini quelconque ou ω.

Règles

The game is played on a finite labelled tree T where the root is marked with a special label (call it +), and every child of root has label 0, and every other node is labeled by any ordinal ≤ ω. This tree is called a hydra.

At each step, we choose a leaf node a to chop off. On the other hand, hydra chooses a nonnegative integer n in some way (for example, it is determined as the number of current step, starting from 1). The hydra alters by the following rules:

1. If a has label 0, we proceed as in Kirby-Paris' game. Call the node's parent b, and its grandparent c (if it exists). First we delete a. If c exists (i.e. b is not the root), we make n copies of b and all its children and attach them to c.
2. If a has label u + 1, we go down the tree looking for a node b with label v ≤ u (which is guaranteed to exist, as every child of the root node has label 0). Consider the subtree rooted at b — call it S. Create a copy of S, call it S'. Within S', we relabel b with u and relabel a with 0. Back in the original tree, replace a with S'.
3. If a has label ω, we simply relabel it with n + 1.

If a is the hydra's rightmost leaf, we notate the transformed tree as T(n).

BH(n) function

Buchholz proved following Theorems (in a sufficiently strong meta theory which proves the consistency of \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) so that the unprovability in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) works):

• Theorem I: By always chopping off the rightmost head, Hercules is able to kill every hydra in a finite number of steps.
• Theorem II: For every fixed hydra A, Theorem I is provable in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).
• Theorem III: Suppose we make a tree with just one branch with \(x\) nodes, labeled \(+,0,\omega,\omega,...,\omega\). Call such a tree \(R^x\). Then it cannot be proven in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\) that for all \(x\), there exists \(k\) such that \(R^x(1)(2)(3)...(k)\) is root tree. (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\).)

Define \(\text{BH}(x)\) as the smallest \(k\) such that \(R^x(1)(2)(3)...(k)\) as defined above is root tree. By Theorem I this function is total on \(\mathbb{N}\) in the meta theory, but by Theorem III the meta theory proves that (the formalisation of) its totality cannot be proven in \(\Pi_1^1-\textrm{CA}+\textrm{BI}\).

Analysis

It is possible to make one-to-one correspondence between some hydras and ordinals.

To convert a tree or subtree to an ordinal:

1. Inductively convert all the immediate children of the node to ordinals.
2. Add up those child ordinals. If there were no children, this will be 0.
3. If the label of the node is not +, apply \(\psi_\alpha\), where \(\alpha\) is the label of the node, and \(\psi\) is fonction de Buchholz.

The resulting ordinal expression is only useful if it is in normal form.

Some examples are:

Hydra	Ordinal
(+)	0
(+(0))	ψ0(0) = 1
(+(0)(0))	ψ0(0) + ψ0(0) = 2
(+(0(0)))	\(\psi_0(\psi_0(0)) = \omega\)
(+(0(0))(0))	\(\psi_0(\psi_0(0)) + \psi_0(0) = \omega + 1\)
(+(0(0))(0(0)))	\(\psi_0(\psi_0(0)) + \psi_0(\psi_0(0)) = \omega 2\)
(+(0(0)(0)))	\(\psi_0(\psi_0(0) + \psi_0(0)) = \omega^2\)
(+(0(0(0))))	\(\psi_0(\psi_0(\psi_0(0))) = \omega^\omega\)
(+(0(1)))	\(\psi_0(\psi_1(0)) = \varepsilon_0\)
(+(0(1)(1)))	\(\psi_0(\psi_1(0) + \psi_1(0)) = \varepsilon_1\)
(+(0(1(0))))	\(\psi_0(\psi_1(\psi_0(0))) = \varepsilon_\omega\)
(+(0(1(1))))	\(\psi_0(\psi_1(\psi_1(0))) = \zeta_0\)
(+(0(1(1(1)))))	\(\psi_0(\psi_1(\psi_1(\psi_1(0)))) = \Gamma_0\)
(+(0(1(1(1(0))))))	\(\psi_0(\psi_1(\psi_1(\psi_1(\psi_0(0))))) = \)SVO
(+(0(1(1(1(1))))))	\(\psi_0(\psi_1(\psi_1(\psi_1(\psi_1(0))))) = \)LVO
(+(0(2)))	ψ0(ψ2(0)) = BHO
(+(0(\(ω\))))	ψ0(ψω(0))