Shawn at Words and Other Things asks about good books on philosophy of logic. If you have suggestions, comment there, please.

Nice! Andrej Bauer has implemented the Hydra Game in a Java applet. The Hydra Game, like Goodstein sequences, is a way of coding ordinals ≤ ε0 ... hence they provide independence results from Peano Arithmetic. Andrej has all the deets. (A Java applet for Goodstein sequences is here.)