The Worm principle

Abstract

In [6] an approach to proof-theoretic analysis of Peano arithmetic based an the motion of graded provability algebra was suggested. Here we present a provability-algebraic version of the independent combinatorial Hydra battle principle. This allows for simple independence proofs of both principles based on provability-algebraic methods.