Résumé | The Hydra game was introduced in 1982 by the mathematicians L. Kirby and J. Paris in their article: "Accessible Independence Results for Peano Arithmetic".
This article contains two theorems:
1. Whichever the strategy of Hercules and the Hydra, any battle eventually terminates with Hercules' victory.
2. The previous result cannot be proved in Peano Arithmetic.
We present a formal, self-contained (axiom-free) proof of a variant of both theorems, with the help of the Coq proof assistant.
Since Coq's logic is higher-order intuitionnistic logic, the reference to Peano Arithmetic is replaced with a study of a class of proofs of termination indexed by ordinal numbers less or equal than epsilon_0.
We present the main parts of this proof, as well as the main features of Coq that made its construction possible. |