Abstract: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{\v s}et{\v r}il). \par After each move of Hercules (trying to kill Hydra fast) there follow $k$ moves of Hidden Hydra Helper (making the same type of moves as Hercules but trying to keep Hydra alive as long as possible). We prove that for $k=1$ Hercules can make the game short, while for $k\geq 2$ Hidden Hydra Helper has a strategy for making the game long.
Keywords: rooted tree, unprovability, Kirby--Paris Theorem
AMS Subject Classification: 05C05, 90D99, 03B25