A New Discovery
Late last week I learned about the Hydra Game. This puzzle has the fairly fantastic property of being un-loseable no matter what strategy you use. What’s even more fascinating is that it isn’t possible to prove that you can’t lose — at least not in the same language as the rules of the game are written.
While the Hydra Game was invented in the early 80s, it was inspired by certain sequences of natural numbers discovered by Goodstein in the 40s. Actually explaining how to generate a Goodstein sequence in the language of arithmetic is somewhat involved, so I’ll just give you punchline: every Goodstein sequence terminates at 0, but there is no way to prove this in the language of arithmetic.
Note that I’m being quite careful always to include to suffixed phrase, “in the language of arithmetic.”
Anyone familiar with Gödel’s incompleteness theorem might hear a few bells going off. A typical example of a Gödel statement is semantically similar to, “Any statement inside quotes in the fourth paragraph of this blog post has no proof.” This disguised self-referential property seems quite unnatural. In fact one might wonder if all true but unprovable statements are self-referential. However, what makes the Goodstein sequences and Hydra Game so fascinating is that they they do not appear to be self-referential.
Starting a New Project
Being so inspired by the deep implications of the Hydra Game, I’m working on a “tree of knowledge” that attempts to describe the major breakthroughs in mathematical logic. The tentative earliest root of the tree is Cantor’s work on set theory in the 1870s and tentative latest leaf is Cohen’s proof the independence of the Axiom of Choice from Zermelo-Franekel Set Theory. I’m hoping this will help guide my study of logic up to the point where I can actually articulate the unprovability of the Hydra Game to a non-technical audience.
This will probably end up being more of a directed acyclic graph than a tree, but that’s somewhat interesting as well given the recent applied research effort into DAGs.
What I’m Reading
Since I read the first 30 pages of GEB before I started taking notes, I’ll give a brief review from memory:
Gödel, Escher, Bach by Douglas R. Hofstadter. Pages 1–30.
The author’s goal is to present the similarities between the musical works of Johannes Bach — in particular his canons and fugues — , the mathematical and logical discoveries of Kurt Gödel, and the mind-bending art of M.C. Escher. To the author, the three titular individuals are “different projections of same object.”
The book takes the form of Dialogue succeeded by Chapter. The Dialogues are somewhat silly and esoteric discussions between various characters. These sections are intended to give the reader an intuition about the ideas presented in the coming chapter. It is a unique to present information and I personally find the book to be quite palatable thus far.
Gödel, Escher, Bach by Douglas R. Hofstadter. Pages 31–51.
The author mentions the desire of mathematicians to prove the consistency of Principia Mathematica. This was one of Hilbert’s 23 problems. The stated goal was the following:
“Was it absolutely clear that contradictory results could never be derived, by any mathematicians whatsoever?”
This question was one of the hottest topics of early 20th century mathematics. Before 1931, it was pretty much assumed that there existed some syntactical formalism which was capable of deriving all of mathematics. Then Gödel proves his incompleteness theorems. Forget the consistency of Principia Mathematica— what Gödel managed to prove was that no system which is capable of describing arithmetic is capable of proving its own consistency.
There is a brief but interesting diversion to discuss Babbage and Lovelace, possibly the first people to envision an automatic computer. Babbage even made references to the “storing” and “milling” of information. Today these ideas are instantiated not as clockwork machines, but rather the RAM and CPUs of modern computers.
At this point the author raises the question of whether humans are inherently separate from machines, pointing out that humans are able to “step outside” of a formal system and make statements about the system itself. He is careful to state that some machines may in fact be capable of stepping outside, but that is definitely true that some are not.
My own personal anecdote: Finding the distinction between machines that can and machines that cannot “step outside” is, to say the least, an interesting problem.
With that, the first chapter begins. Hofstadter introduces the MU system, a very simple example of a formal system. In it, certain strings of characters can be “built” by starting from a given string and then modifying the string according to some definite rules. The question is then, can you build the string “MU” starting from the string “MI”?
Correlations are then drawn between the axioms of a formal language and the starting strings of the MU system. Likewise, the relation between rules of inference in logic and the rules of string manipulation in MU is expounded upon. Finally, the author points out the difference between working inside the system, where you manipulate strings according to the given rules, and working outside the system, where you make statements about which strings are possible and which are not. This ties back to the question of determining which aspects of logic are purely mechanical and which aspects require that je ne sais quoi we call insight.