Hercules and Hydra
Hercules and Hydra, a game on rooted finite trees
Hercules versus Hidden Hydra Helper
L. Kirby and J. Paris introduced the Hercules and Hydra game on rooted trees as a natural example of an undecidable statement in Peano Arithmetic. One can show that Hercules has a “short” strategy (he wins in a primitively recursive number of moves) and also a “long” strategy (the finiteness of the game cannot be proved in Peano Arithmetic). We investigate the conflict of the “short” and “long” intentions (a problem suggested by J. Nešetřil). After each move of Hercules (trying to kill Hydra fast)...