17 May 2008

Amusing discovery

The Columbia University formal ontologist Achille Varzi, co-author (with Roberto Casati) of Parts and Places and Holes and Other Superficialities, shares a name with (and, according to Wikipedia, is related to) the (seemingly rather famous) Italian racing driver Achille Varzi, winner of the 1933 Monaco Grand Prix, whose death during practice in 1948 led to the imposition of mandatory crash helmets in automobile racing.

11 May 2008

Information-age idioms

A remarkable phrase encountered in Wikipedia: 'Turing porn farm'.

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.

29 April 2008

Found

"Jacques Herbrand aurait détesté Bourbaki."
--Claude Chevalley

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.