Now here is the weird and confusing part. If the above is a valid proof, then H will eventually find it. It searches all proofs, remember?

Fortunately, H will never find your argument because it is not a correct proof. You rely on hidden assumptions of the following form (given informally and symbolically):

 If φ is provable, then φ holds.
Provable(#φ) → φ

where #φ denotes the Gödel number of the proposition φ.

Statements of these form are generally not provable. This phenomenon is known as Löb's theorem - featured in Main back in 2008.

You use these invalid assumptions to eliminate the first two options from Either H returns true, or false, or loops forever. For example, if H returns true, then you can infer that "FF halts on input FF" is provable, but that does not contradict FF does not halt on input FF.

Just calling the problem undecidable doesn't actually solve anything. If you can prove it's undecidable, it creates the same paradox. If no Turing machine can know whether or not a program halts, and we are also Turing machines, then we can't know either.

I guess the answer to this point is that when constructing the proof that H(FL, FL) loops forever, we assume that H can't be wrong. So we are working in an extended set of axioms: the program enumerates proofs given some set of axioms T, and the English-language proof in the tumblr post uses the axiom system T + "T is never wrong" (we can write this T+CON(T) for short).

Now, this is not necessarily a problem. If you have reason to think that T is consistent, then most likely T+CON(T) is consistent also (except in weird cases). So if we had some reason to adopt T in the first place, then working in T+CON(T) is also a reasonable choice. (Note that this is different from working in a system which can prove its own consistency, which would be bad. The difference is that in T+CON(T), there is no way to prove that proofs using the additional "T is never wrong" axiom are correct).

More generally, the lesson of Gödel's incompleteness theorem is that it does not make sense to say that something is "provable" without specifying which proof system you are using, because there are no natural choice for an "ideal" system, they are all flawed. The tumblr post seems paradoxical because it implicitly shifts between two different axiom sets. In particular, it says

If there is no way for H to prove whether it halts or not, then we can’t prove it either.

but a correct statement is, we can't prove it either using the same set of axioms as H used. We have to use some addtional ones.

Therefore a proof that it doesn't halt does exist (this one), and it will eventually find it.

Gödel's incompleteness bites here. What theory is your halt-testing machine H searching for a proof within? H can only find termination proofs that are derivable from the axioms of that theory. What theory is your proof that H(FL,FL) does not terminate expressed in? I believe it will necessarily not be the same one.

It does not give a counterexample. It specifies a way that you could find a counterexample if there was a halting oracle. But if there was a halting oracle there wouldn't be any counterexample. So what is found is a contradiction.

EDIT: Okay, now I read your article, and I see that what I wrote here is irrelevant. Leaving it here anyway, maybe someone else will like it.

I admit I didn't read your linked article thoroughly, but I will try to explain the basic theory and terminology.

In computer science, when we are talking about a computation that for any input always ends in a finite time and provides an answer, we call such computation algorithm, and the mathematical function computed by this algorithm is called "total recursive function" (or "computable function").

When we are talking about a computation that could potentially run forever, and such case of running forever is treated as an implied special value, we call such computation program, and the mathematical function computed by this algorithm is called "partial recursive function" -- a mathematical function with an undefined value for inputs where the program runs forever. (Algorithms are a subset of programs, and total recursive functions are a subset of partial recursive functions.)

Specifically, if we care about computations returning "yes" or "no", an algorithm corresponds to a total recursive function from X to { "yes", "no" }, where "X" is the input domain: strings, numbers, whatever your computation accepts as a valid input. If we care about computations that potentially run forever, such program corresponds to a partial recursive function from X to { "yes" }, where not returning value is an implied "no". (You could have other, equivalent definitions, but that would only make things less elegant mathematically.)

When debating things such as Halting Problem we have to pay extra big attention to the proper distinction between algorithms and programs, or respectively between total and partial recursive functions. When speaking about programs / partial recursive functions we have to pay attention to which answer is the implied one in case of the infinite computation (is "yes" explicit and "no" implied, or is "no" explicit and "yes" implied?). A simple mistake can change everything dramatically. For example:

Q1: "Can we make an algorithm which, given an arbitrary program and an arbitrary input for that program, determines whether the program will stop in finite time?"

A1: "No. See the standard debate about Halting Problem."

Q2: "Can we make a program which, given an arbitrary program and an arbitrary input for that program, determines whether the program will stop in finite time?"

A2: "Yes, trivially. Just simulate the given program, and print "yes" if the simulation stops."

Q3: "Can we make a program which, given an arbitrary program and an arbitrary input for that program, determines whether the program will run forever?"

A3: "No. If such program would be possible, then together (running in parallel) with the previous program they would make an algorithm solving the Halting Problem, which we already know is mathematically impossible."

I believe that if you will be very careful about which of these words you use, the confusion will be solved. In my opinion, most likely at some place you proved that a program exists for something, but then you started treating it as an algorithm.

No, it's the halting problem all the way down.

But if it's true that there doesn't exist a proof that it halts, then it will run forever searching for one.

Not remotely! There's no proof that it halts, and there's no proof that it doesn't halt. It will run until it halts or the universe ends - there is no forever. The key is that there can be programs for which nobody can tell which one they are without actually trying them until they halt or the universe ends.

Okay, an attempt to clear up the Halting Problem:

The proofs in question say it is impossible to algorithmically arrive at a Yes-or-No answer to the generalized question, "Does algorithm X have non-trivial property Y for input Z?", for any specific property Y. Poorly written proof at the bottom. It critically doesn't say that you can't have a Yes-or-No-or-Undecidable answer to that question. Introduce an uncertainty factor and the issue falls apart. Thus, you -can- write a Halting Oracle, so long as you're satisfied that sometimes it won't be able to say.

For purposes of AI Friendliness - which is certainly a non-trivial property - Rice's Theorem says we can't algorithmically prove that an AI - which is an algorithm - is, or is not, friendly, once we manage to define what friendly even is. We can theoretically, however, prove that AI is friendly, not friendly, or undecidably friendly. For our purposes, "not friendly" and "undecidably friendly" are probably equivalent.

For purposes of everything else, nothing at all says that it's impossible to prove whether or not a specific program will halt given a specific input. "But what about the program in Turing's diagonalization proof? Does it halt or not?" The input in that case (the Halting Oracle) can't exist in the first place, as the proof demonstrates.

"But what about this neat program I wrote that halts 25% of the time?" What did you use to generate a random number? Not being aware of your hidden inputs isn't the same as not having an input. For a given set of inputs, your algorithm halts 100%, or 0%, of the time.

A Halting Oracle that only says "Yes", "No", or "Provably Undecidable" hasn't (to my knowledge and research) been proven to be impossible - and a "Yes", "No", or "Maybe" Halting Oracle is quite trivial, as you can throw all cases you can't figure out an algorithm for into the "Maybe" pile. The proofs do not demonstrate that there are any algorithms which are nondeterministically halting for a given input, nor do they demonstrate that we can't prove that any given algorithm will or will not halt, nor do they even demonstrate that an algorithm can't prove that other algorithms will or will not halt - they demonstrate one thing and one thing only, and that is that there is no single algorithm which gives a "Yes" or "No" answer will work on all algorithms for all inputs.

An equivalent-to-Rice's-Theorem-for-our-very-limited-purposes-proof written like the halting problem proof. A trivial property in this case means it -can- vary by algorithm and input.

Suppose Algorithm Zed determines whether or not Algorithm X has non-trivial property Y for the input Z, returning a boolean value. Take Algorithm ScrewZed, with an input of AlgorithmZed, which has the non-trivial property Y iff its evaluation of AlgorithmZed, given the input of Algorithm ScrewZed with the input of AlgorithmZed, says it doesn't have non-trivial property Y. Paradox ensues, provided I wrote all this correctly.

If you can prove it's undecidable, it creates the same paradox.

What makes you say this?

Also, there is definitely some objective fact where you cannot get the right answer:

"After thinking about it, you will decide that this statement is false, and you will not change your mind."

If you conclude that this is false, then the statement will be true. No paradox, but you are wrong.

If you conclude that this is true, then the statement will be false. No paradox, but you are wrong.

If you make no conclusion, or continuously change your mind, then the statement will be false. No paradox, but the statement is undecidable to you.

From the link:

That means that we can’t actually prove that a proof doesn’t exist, or it creates a paradox. But we did prove it! And the reasoning is sound! Either H returns true, or false, or loops forever. The first two options can’t be true, on pain of paradox. Leaving only the last possibility. But if we can prove that, so can H. And that itself creates a paradox.

H proves that it can't decide the question one way or the other. The assumption that H can only return TRUE or FALSE is flawed: if a proof exists that something is undecidable, then H would need to be able to return "undecidable".

This example seems to verify the halting problem: you came up with an algorithm that tries to decide whether a program halts, and then came up with an input for which the algorithm can't decide one way or another.

But if it's true that there doesn't exist a proof that it halts, then it will run forever searching for one.

No; provable and true are not the same thing. It may be the case that the program halts, but it is nevertheless impossible to prove that it halts except by "run it and see", which doesn't count.

There is no program such that no Turing machine can determine whether it halts or not. But no Turing machine can take every program and determine whether or not each of them halts.

It isn't actually clear to me that you a Turing machine in the relevant sense, since there is no context where you would run forever without halting, and there are contexts where you will output inconsistent results.

But even if you are, it simply means that there is something undecidable to you -- the examples you find will be about other Turing machines, not yourself. There is nothing impossible about that, because you don't and can't understand your own source code sufficiently well.