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 \(phi : {cal N} times {cal N} rightarrow {cal N}\). 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 \(phi\). So if you wanted to describe running the program "\(f\)" on the input 7, you'd write that as \(phi(f, 7)\). And, finally, the way that we would write that a program \(p\) doesn't halt for input \(i\) as \(phi(p, i) = bot\).

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: \(langle x,yrangle\).

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

\[forall p, forall i: (varphi(O,langle p,irangle) = left{

begin{array}{l}

0 mbox{ if } varphi(p, i) = bot \

1 mbox{ if } varphi(p,i) neq bot

end{array}

right.

\]

In english, does there exist a program \(O\) such that for all pairs of programs p and inputs i, the oracle returns \(1\) if \(varphi(p, i)\) 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 \(p\) and input \(i\), \(varphi(O, langle p, i rangle) = 0 iff varphi(p,i)=bot\).

So, can we devise a program $p_d$ and input \(i\) where \(varphi(p_d, i) != bot\),

but \(varphi(O, langle p, i rangle) = 0\)?

Of course we can. We need a \(p_d\) 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, \(p_d\) 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 \(O\) will incorrectly predict the halting status? So what we'll do is just turn \(p_d\) into a parameter to itself. That is, we'll look at a program \(p_d\) 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, \(p\), there are an *infinite* number of versions of the same program with different Gödel numbers. Using that property, you can embed a program \(p_{d_2}\) into another program \(p_{d}\). 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 = \(langle O, p_d rangle\), then \(O\) will make the *wrong* prediction about what \(p_d\) 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.