A remarkable phrase encountered in Wikipedia: 'Turing porn farm'.
11 May 2008
The hydra game
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.
29 April 2008
A note
Somewhere in the Platonic heaven of unwritten doggerel, there is a poem rhyming venia legendi with venial effendi. I learned of it, as Mr Humbert learned of genuflection lubricity, from a sign sleeping by the road.
16 March 2008
Tree diagrams
Does anyone know of a simple programme for producing tree diagrams (analogous to those used by linguists, although frequently with more complex labels on the nodes, including labels involving multiple lines and logical or mathematical formulae) ? I'm currently using phpSyntaxTree, which is better than trying to draw the trees in Word, but not great.
09 March 2008
An Interesting Article in the Times
Somehow I missed this when it came out, in November.
Apparently there's been serious debate in the U.S. State and Defense Departments over whether the U.S. should share permissive action link (PAL) technology with Pakistan.
For background on PALs, see here and here.
It seems that this would be a good step towards improving Pakistan's nuclear security. The U.S. itself has not always been exemplary in this area: for a very long time, weapons on Navy submarines did not have PALs.
Apparently there's been serious debate in the U.S. State and Defense Departments over whether the U.S. should share permissive action link (PAL) technology with Pakistan.
For background on PALs, see here and here.
It seems that this would be a good step towards improving Pakistan's nuclear security. The U.S. itself has not always been exemplary in this area: for a very long time, weapons on Navy submarines did not have PALs.
19 January 2008
Subscribe to:
Posts (Atom)
