Worms, gaps, and hydras. (English)
Math. Log. Q. 51, No. 4, 342-350 (2005).
Summary: We define a direct translation from finite rooted trees to finite natural functions which shows that the Worm Principle introduced by Lev Beklemishev is equivalent to a very slight variant of the well-known Kirby-Paris Hydra Game. We further show that the elements in a reduction sequence of the Worm Principle determine a bad sequence in the well-quasi-ordering of finite sequences of natural numbers with respect to Friedman’s gap-embeddability. A characterization of gap-embeddability in terms of provability logic due to Lev Beklemishev is also presented.