Just keep asserting, just keep asserting

About fifteen years ago, I attended a talk by Roger Penrose at the Edinburgh Science Festival on the topic of Gödel’s incompleteness theorem. After Penrose finished delivering the talk, an elderly gentleman in the audience stood up and said that he didn’t really see what the fuss was about. You shouldn’t worry, he asserted, that it’s been shown that every formal system has a ‘tricky’ statement (ie. true but not provable). Chances are, it’s not a very interesting statement. And, besides, if you really cared about it, you could just extend your formal system to assert that it’s true. “Ahh”, said Penrose, “but now that new system you’ve created will have it’s own unprovable statement!”. The elderly gentlement was not impressed. “Well then”, he said, “I’d just add a new rule to that one too!”. Penrose noted that the augmented system would suffer the same incompleteness fate, but the elderly gentleman was prepare to keep adding more rules for as long as it took, and the session briefly descended into farce.

At the time, I thought the guy was missing the point. After all, it’s the incompleteness of any given formal system which matters – patching the formal systems with duct tape moves the goal posts but doesn’t let you escape the problem.

But, with a more engineering mindset on today, what he said seems quite reasonable. Most of the time, the incompleteness or undecidability of a formal system doesn’t stop you doing lots of interesting things with it. I don’t worry about the halting problem when I start up firefox, and my high school maths teacher seemed unconcerned that my homework submissions might contain a true-but-unprovable statement. I’m also reminded of a quote I read a long time ago in a paper about the dependently-typed language, Cayenne:

“So type checking Cayenne is undecidable. This is unfortunate, but unavoidable for a language like Cayenne. How bad is it in practice to have an undecidable type checker? This question can only be answered by practical experiments. The Cayenne programs we have tried to date range from ordinary Haskell style programs, to programs using dependent types, to proofs of mathematical propositions. The total size of these programs are only a few thousand lines, but so far the experience shows that it works remarkably well.

Having undecidable type checking means that the type checker might loop. This is clearly not a user friendly type checker. So instead the implemented type checker has an upper bound on the number of reduction steps that it may perform. If this limit is exceeded the type checker will report this. Most of the type errors from the Cayenne compiler are similar to those that any other language would give. Very infrequently does the type checker report that it did not terminate within the prescribed number of steps. Most often, this is the result of a type error, but sometimes the type expression is just too complicated and the number of reduction steps must be increased (the number of reduction
steps is a compiler arg).”

Anyhow, to come full circle, the reason that I remember all this tonight is that I just found out that Alan Turing’s thesis was on exactly the topic which the elderly gentleman was riffing on. In essence, what happens when you keep patching your formal system, Wily Coyote stylee, to build an ACME infinite series of formal systems, each a litle bit better that the one before? I have not read the thesis yet, but I found it amusing to note that, with hindsight, the eldery gentleman from fifteen years ago was onto something!