# The Samovar

Nice new proof of Godel’s theorem
March 24, 2007, 2:18 pm
Filed under: Mathematics

I’ve had this sitting around for a while. Harvey Friedman wrote a new proof of Godel’s theorem on the FOM mailing list. I’m writing this entry so that I have a reminder of it for myself, but others might find it interesting too.

Intuitively speaking, Godel’s theorem says that every mathematical system has statements which are true but can’t be proved within that system. The normal way to think of this is that you can’t prove the statement “This statement cannot be proved” but nonetheless it’s true. You can’t prove it because if you could it would be true, and then it would say that you couldn’t prove it which would be a contradiction. But it must be true, because if it was false then there would have to be a proof of it, and so it would have to be true, which is a contradiction. This might seem reminiscent of the paradoxical sentence “This sentence is false”, but there is a subtle difference which I probably don’t want to go into in too much detail here. (The difference between truth and provability.)

Friedman’s proof uses Turing machines. Without going into any technical details – a Turing machine is basically just a computer program. A computer program can be represented as a single number. Just take the file on your computer; it’s a string of 1s and 0s, which is just a (very large) number in binary. So we can number every possible computer program. Write TM[n] for the computer program whose corresponding number is n. Actually, I’m going to restrict myself to computer programs which take one input (say the number m), and return one output. Given some computer program and an input m, the program may never stop running. For example, the program

```DO

LOOP```

never stops running. The custom when talking about Turing machines is to say that the program doesn’t halt.

So here is Friedman’s proof. We write a computer program P that does the following: Given an input m,  it searches for a proof that “TM[m] does not halt when given input m”. That is, it searches for a proof that program m, when given input m, will eventually stop running and return some number. If there is a proof, then P will eventually find it, otherwise P itself will not stop running.

Here’s where it gets clever. The program P is itself just a computer program that takes a single input m, and so it must have a number, call that number k. In other words, P=TM[k] for some number k. Keep that in mind.

So what happens if we run program P with input k? We can work this out by considering two alternatives. Either there is or isn’t a proof of the statement “TM[k] does not halt when given input k”. If there is a proof then running program P with input k will find the proof, and therefore this program halts at input k. But we’re assuming that there is a proof that “P=TM[k] does not halt at input k”, so this is a contradiction.

Therefore, there is no proof that “TM[k] does not halt at input k”, but nonetheless it is true.

If you want to know more (that’s just a very sketchy and technically inaccurate overview), then take a look at Harvey’s message to FOM above. If you want to understand it but can’t (e.g. you might ask yourself having read it: what is PA and what is Con(PA)?) , just post a message here. If you found it interesting, you might also be interested in reading up on The Halting Problem (which is closely related).