ABSTRACT

Here we present a simple statement of combinatorial nature that is indepen­ dent of Peano arithmetic and is motivated by the provability algebraic view of so. The principle asserts the termination of a certain combinatorial game similar to the well-known Hydra battle of L. Kirby and J. Paris [11] which we call the Worm battle. In fact, modulo some details, the Hydra principle and the Worm principle turn out to be mutually translatable and one can easily infer the independence of the one from that of the other.1 Thus, we essentially provide an alternative proof of the Kirby-Paris independence result. How­ ever, the Worm principle also has some independent interest because of the naturality of its provability algebraic interpretation.