[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #23 (Solved !)

Originator: E. A. Cichon [Cic90]
Date: April 1991

Summary: Must any termination ordering used for proving termination of the Battle of Hydra and Hercules-system have the Howard ordinal as its order type?

The following system [DJ90], based on the “Battle of Hydra and Hercules” in [KP82], is terminating, but not provably so in Peano Arithmetic:


Transfinite (є0-) induction is required for a proof of termination. Must any termination ordering have the Howard ordinal as its order type, as conjectured in [Cic90]?


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].


This has been answered to the negative by Georg Moser [Mos09], by giving a reduction order that is compatible with the above rewrite system, and whose order type is at most є0 (the proof theoretic ordinal of Peano arithmetic).


E. A. Cichon. Bounds on derivation lengths from termination proofs. Technical Report CSD-TR-622, Department of Computer Science, University of London, Surrey, England, June 1990.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.
Laurie Kirby and Jeff Paris. Accessible independence results for Peano arithmetic. Bulletin London Mathematical Society, 14:285–293, 1982.
Georg Moser. The Hydra battle and Cichon’s principle. Applicable Algebra in Engineering, Communication and Computing, 20(2):133–158, 2009. doi:10.1007/s00200-009-0094-4.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]