Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence

Authors Sarah Winkler, Harald Zankl, Aart Middeldorp

Thumbnail PDF


  • Filesize: 0.53 MB
  • 17 pages

Document Identifiers

Author Details

Sarah Winkler
Harald Zankl
Aart Middeldorp

Cite AsGet BibTex

Sarah Winkler, Harald Zankl, and Aart Middeldorp. Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 335-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano (1889) arithmetic. We present an encoding of Goodstein's theorem as a termination problem of a finite rewrite system. Using a novel implementation of ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiple recursive. Our method can also cope with the encoding by Touzet (1998) of the battle of Hercules and Hydra, yet another system which has been out of reach for automated tools, until now.
  • term rewriting
  • termination
  • automation
  • ordinals


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail