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.