The Worm principle is a version of the well-known Hydra battle principle that was motivated by a novel ordinal notation system for epsilon_0 coming from graded provability algebras.

The Worm Principle

A finite function f:[0,n] -> N (natural numbers) is called a Worm. (We picture the Worm as hovering in the air above the ground, which is at level 0.) We can also think of it as of a sequence of natural numbers. The head of the Worm is f(n), f(0) is its tail. At every stage of the game the head of the Worm is deleted, but then, unless f(n)=0, the Worm grows. The rules of growth are as follows.

Assume f(n)>0 and we are at Stage k of the game. Let m<n be the maximal number such that f(m)<f(n). We delete the head and attach to the remaining part of the Worm the sequence (f(n)-1) f(m+1)...f(n-1) taken k times followed by the new head (f(n)-1).

Claim: The statement

Every Worm is eventually being eliminated

is true but unprovable in Peano Arithmetic.

The proof has not yet been published, but it is not difficult on the basis of the results in

Beklemishev, L.D. (200?): Provability algebras and proof-theoretic ordinals, I. Department of Philosophy, Utrecht University, Logic Group Preprint Series 208, March 2001, to appear in Annals of Pure and Applied Logic.

In fact, the Worms are precisely the ordinal notations from that paper. See also my LC 2002 tutorial slides.

A. Weiermann investigated the fine tuning of many combinatorial principles w.r.t. some built-in parameters. In this case, we demand that a certain part of the Worm be copied k times. Instead we can consider a variant, where one copies it only [c.log(k)] times, for some constant c. ([...] means the integer part.) I conjecture an optimal result of the following kind. There is a constant c such that, if one copies it [c₁log(k)] times for c₁<c, then the Worm principle is provable, otherwise, it is unprovable. Find the constant c.

Even if this conjecture fails for the log function, it may still hold for some slowlier growing function of k.