Gödel, Turing and decidability


Portrait of Kurt Gödel, one of the most signif...
Image via Wikipedia

I am still wandering around in the world opened to me by The Annotated Turing
– perhaps a little lost, but I have been reading some guide books.

The most recent of these has been Gödel’s Proof which gives a gentle(ish) introduction to Gödel’s incompleteness theorem.

This is a short, but fascinating book that I repeatedly made the mistake of trying to read when tired or not able to give it my full attention (eg on a flight from London to Budapest last week when three days of hard work had really taken it out of me). But I finally managed to finish it last night.

I think the really startling point it makes – which admittedly Charles Petzold’s book also makes but I didn’t fully grasp at the time – is about the nature of the human mind.

Gödel’s theorem states that no consistent system of axioms whose theorems can be listed by an “effective procedure” (such as a computer program) is capable of proving all facts about the natural numbers.

Before I read the book I had not really thought about what this meant: after all Turing and Church had shown that most numbers/mathematical problems were not computable and so this seemed of a part with that conclusion.

But the key thing here is that metamathematics can show the correctness of theorems that axiomatic proofs cannot. In other words – I think – that computer programs are actually a poor model of our ability to solve mathematical problems.

Coming up… the lambda calculus


An example of a DFA state diagram
Image via Wikipedia

Another thing that The Annotated Turing taught me is what all those lambdas that I have seen over the last 25 years were about, or at least it introduced me to what they were about.

So I have just ordered a copy of Structure and Interpretation of Computer Programs: and I can guess that some blog posts will eventually follow.

Oh no. Maybe I am turning into a LISP hacker – having finally reached the age that all these guys were when I first became aware of them (older, actually).