Andrej Bauer has a superb page on the hydra game, including a Java applet allowing you to play it. The hydra game is extraordinarily simple: the rules can be stated in a few sentences. A hydra is a finite tree: the object of the game is to cut off all of its nodes ("heads"). If you cut off a node at level 1, it does not grow back. If you cut off a node at level n > 1, the hydra grows new branches from the node two levels down -- duplicates of the subtree growing out of level n-1, the direct parent node, after the level-n node has been removed. The proof, in set theory, that every hydra can be killed, is beautiful and almost as short as this description -- the game is just Goodstein's theorem (1948) differently, and much more elegantly, phrased.
But that's not the remarkable thing. The remarkable thing, demonstrated in 1982 by Kirby and Paris, is that any proof of Goodstein's theorem requires transfinite induction up to epsilon-zero or its equivalent -- which is the consistency strength of Peano Arithmetic. So, by Gödel's second incompleteness theorem, it is impossible to prove in PA that the hydra game is always winnable.
I am astounded that a "mathematically natural" statement independent of PA (as opposed to a Gödel sentence tricked up for the purpose of proving incompleteness) is capable of such an exquisitely simple, intuitively appealing formulation.
But that's not the remarkable thing. The remarkable thing, demonstrated in 1982 by Kirby and Paris, is that any proof of Goodstein's theorem requires transfinite induction up to epsilon-zero or its equivalent -- which is the consistency strength of Peano Arithmetic. So, by Gödel's second incompleteness theorem, it is impossible to prove in PA that the hydra game is always winnable.
I am astounded that a "mathematically natural" statement independent of PA (as opposed to a Gödel sentence tricked up for the purpose of proving incompleteness) is capable of such an exquisitely simple, intuitively appealing formulation.
No comments:
Post a Comment