Some people expressed interest in seeing a full-out, formal presentation of the Halting problem proof. So, I’m going to walk through it. There are actually a lot of different versions of this proof; the one that I’m going to use is based on the one used by my grad-school theory professor, Dr. John Case. To be clear, I’m doing it from memory, so any errors are completely my own fault, not John’s!

To start off, we need to define what a computing device is. In formal mathematical terms, we don’t care how it works – all we care about is what it can do in abstract tems. So what we do is define something called an effective computing device. An effective computing device is any Turing equivalent computing device. An ECS is modelled as a two parameter function . The first parameter is an encoding of a program as a natural number; the second parameter is the input to the program. It’s also a natural number, which might seem limiting – but we can encode any finite data structure as an integer, so it’s really not a problem. The return value is the result of the program, if the program halts. If it doesn’t halt, then we say that the pair of program and input aren’t in the domain of . So if you wanted to describe running the program “” on the input 7, you’d write that as . And, finally, the way that we would write that a program doesn’t halt for input as .

So now we’ve got our basic effective computing device. There’s one thing we still need before we can formulate the halting problem. We need to be able to deal with more parameters. After all – a halting oracle is a program that takes two inputs – another program, snd the input to that program. the easiest way to do that is to use something called a pairing function. A pairing functions is a one-to-one function from an ordered pair to an integer. There are lots of possible pairing functions – for example, you can convert both numbers to binary, left-pad the smaller until they’re equal length, and then interleave the bits. Given (9,3), you convert 9 to 1001, and 3 to 11; then you pad 3 to 0011, and interleave them to give you 10001011 – 139. We’ll write our pairing function as angle brackets around the two values: .

With the help of the pairing function, we can now express the halting problem. The question is, does there exist a program , called a halting oracle, such that:

In english, does there exist a program such that for all pairs of programs p and inputs i, the oracle returns if halts, and 0 if it doesn’t?

Time, finally, for the proof. Suppose that we do have a halting oracle, O. That means that for any program and input , .

So, can we devise a program $p_d$ and input where ,
but ?

Of course we can. We need a which takes two parameters: an oracle, and an input. So it should be really simple right? Well, not quite as easy as it might seem. You see, the problem is, needs to be able to pass itself to the oracle. But how can it do that? A program can’t pass itself into the oracle. Why not? Because we’re working with the program as a Gödel number – and a program can’t contain its own Gödel number. If it contained it, it would be larger than itself. And that’s rather a problem.

But there’s a nice workaround. What we care about is: is there any combination of program and input such that will incorrectly predict the halting status? So what we’ll do is just turn into a parameter to itself. That is, we’ll look at a program like the following:

def deceiver(input):
   (oracle, program) =  unpair(input)
   if oracle(program, input):
      while(True): continue
   else:
      halt

Then we’ll be interested in the case where the value of the program parameter is a Gödel number of the deceiver itself.

(As an aside, there are a variety of tricks to work around this. One of the more classical ones is based on the fact that for any given program, , there are an infinite number of versions of the same program with different Gödel numbers. Using that property, you can embed a program into another program . But there are a few other tricks involved in getting it right. It’s not simple – Alan Turing screwed it up in the first published version of the proof!)

Now, when input = , then will make the wrong prediction about what will do. So – once again, we’re back where we were in the simpler version of the proof. A halting oracle is a program which, given any pair of program and input, will correctly determine whether that program will halt on that input. We’re able to construct a pair of program and input where the oracle doesn’t make the right prediction, and therefore, it isn’t a halting oracle.

This version is more abstract, but it’s still got that wonderfully concrete property. Even in the most abstract way of talking about a computing device, if you’ve got something that you believe is a halting oracle, this shows you how to create a program that will prove that the halting oracle is wrong. So you can’t possibly create a halting oracle.

And to be extra clear: this doesn’t rely on any ambiguities about definitions, or any distinction between values and meanings. It shows a way of producing a real, concrete counterexample for any purported halting oracle. No trickery, no fudging – if you think you have a halting oracle, you’re wrong, and this proof shows you exactly how to create a program that will demonstrate that.