### The Hydra Battle and Cichon’s Principle

Georg MoserApplicable Algebra in Engineering, Communication and Computing 20(2), pp. 133 – 158, 2009.

### Abstract

In rewriting the Hydra battle refers to a term rewrite system

H proposed by Dershowitz and Jouannaud. To date, H withstands

any attempt to prove its termination automatically. This motivates

our interest in term rewrite systems encoding the Hydra battle,

as a careful study of such systems may prove useful in the design

of automatic termination tools. Moreover it has been an open

problem, whether any termination order compatible with H has to

have the Howard-Bachmann ordinal as its order type, i.e., the proof

theoretic ordinal of the theory of one inductive definition. We

answer this question in the negative, by providing a reduction order

compatible with H, whose order is at most epsilon_0, the proof

theoretic ordinal of Peano arithmetic.

### BibTeX

@article{GM-AAECC09, author = "Georg Moser", title = "The {H}ydra {B}attle and {C}ichon's {P}rinciple", journal = "Applicable Algebra in Engineering, Communication and Computing", volume = 20, number = 2, year = 2009, pages = "133--158" }