I'm wondering if anyone is aware of a proof of the Halting Problem that is not just a permutation of the "standard" proof. Since there are so many formulations of this proof, rather than pick a specific one, I will sketch out the general outline that every proof I've seen follows (at least, I honestly don't remember one that doesn't follow this pattern):

1. Assume that there is a function halt() that can decide whether or not a given Turing Machine halts or not.
2. Construct a Turing Machine that embeds halt(), but "does the exact opposite".
3. ...
4. Proof by contradiction that because we have constructed a program that embeds halt(), but does the exact opposite, this proves that halt() can not exist.

I believe the above is "sufficiently accurate" for the purposes of this question. Please feel free to speak up if you feel it misses some nuance of the problem and / or proof.

My objection with this entire class of proofs is:

• Every formulation of the problem / proof begins by assuming that halt() exists and is capable of deciding whether or not a given Turning Machine halts or not.

At this point in the proof, there are really only two possibilities:

1. halt() does not, or can not, decide whether a Turing Machine halts or not.
2. halt() can, and does, decide whether or not a Turing Machine halts.

The problem is this: If we choose the first possibility, that is to say that for some unspecified reason halt() does not "work as advertised", the proof comes to an end. There is literally no point in proving halt() can not decide whether a Turing Machine halts or not if we handicap it from the start- we already know the answer.

I'm not aware of any proof that places qualifications on halt() at this point in the proof, therefore the only reasonable choice is the second possibility. This means that we axiomatically define halt() in order to "bring it in to existence". The problem with this is- halt() is axiomatically defined, and therefore is guaranteed to decide whether or a Turing Machine halts or not.

Since halt() is axiomatically defined as being able to decide whether a Turing Machine halts, any analysis that arrives at a result that contradicts this behavior can not, by definition, prove that halt() is undecidable. The axiomatic definition of halt() is so strong that any result that causes, or results in, a contradiction of halt() is proof that the hypothesis is invalid. Basically, just like the first possibility, there's no point in continuing on with the proof with this choice either because we have our answer- it is impossible to prove that the Halting Problem is undecidable using this technique because it is axiomatically guaranteed to be decidable.

Therefore, I personally consider this family of Halting Problem proofs to be invalid.

So, I'm wondering if anyone is aware of a proof of the Halting Problem that is "independent" of this style and family of proof. I have a strong preference for a proof that does not rely on "diagonalization" or "recursion" in any way. My preference is for something rooted in graph theory.

Which raises a different problem: So far, I have been unable to arrive at a zero-order approximation of a Halting Problem proof using other means. In fact, every back of the envelope attempt has completely failed to arrive at the same conclusion.

The strongest one I've managed to come up with is roughly: The $\delta$ transition table is finite, with a finite number of symbols. An appeal to König's lemma seems to be enough to justify that there is no infinite path, and therefore it must be possible to find a path from the start state to a halting state, if one exists. Not intended as proof, but a result from graph theory, whatever it is, would be much stronger than the current "Say something is true, then do the exact opposite, and then claim that by doing the exact opposite of what you first claimed, you've proved that it was never true to begin with" proof.

Does anyone:

1. Have a Halting Problem proof that is significantly different than the current "standard" proof? My preference is for a proof that gives the same result using completely different techniques and / or approach. So far, I have only been able to find derivatives of the "standard" proof.
2. See a problem with the analysis above?