\documentclass{rtaloop}
\rtalabel{hydra}
\begin{document}
\begin{solvedproblem}{E. A. Cichon}{\cite{C90:london}}{April 1991}
\begin{abstract}
Must any termination {\em ordering\/} used for proving termination of the
\emph{Battle of Hydra and Hercules}-system have the Howard ordinal as its
order type?
\end{abstract}
The following system \cite{DJ90:htcs}, based on the
``Battle of Hydra and Hercules'' in \cite{KP82:lms},
is terminating, but not provably so in Peano Arithmetic:
\begin{eqnarray*}
h(z,e(x)) & \rightarrow & h(c(z),d(z,x))\\
d(z,g(0,0)) & \rightarrow & e(0)\\
d(z,g(x,y)) & \rightarrow & g(e(x),d(z,y))\\
d(c(z),g(g(x,y),0)) & \rightarrow & g(d(c(z),g(x,y)),d(z,g(x,y)))\\
g(e(x),e(y)) & \rightarrow & e(g(x,y))
\end{eqnarray*}
Transfinite ($\epsilon_0$-) induction is required for a proof of termination.
Must any termination {\em ordering\/} have the Howard ordinal as its order
type, as conjectured in \cite{C90:london}?
\begin{remark}
If the notion of termination ordering is formalized by using ordinal
notations with variables, then a termination proof using such
orderings yields a slow growing bound on the lengths of derivations.
If the order type is less than the Howard-Bachmann ordinal then, by
Girard's Hierarchy Theorem, the derivation lengths are provably
total in Peano Arithmetic. Hence a termination proof for this
particular rewrite system for the Hydra game cannot be given by such
an ordering [Andreas Weiermann, personal communication].
\end{remark}
\begin{remark}
This has been answered to the negative by Georg
Moser~\cite{moser:aaecc2009}, by giving a reduction order that is
compatible with the above rewrite system, and whose order type is at
most $\epsilon_0$ (the proof theoretic ordinal of Peano arithmetic).
\end{remark}
\end{solvedproblem}
\end{document}