I'm following through the proof of the impossibility of the Halting problem for the umpteenth time. It all makes sense logically, but not intuitively. A question I got stuck on:
Suppose we built the following machine in attempt to solve the halting problem. It takes our standard set of axioms (ZFC, let's say, or Peano arithmetic, or whatever) and first tries every one-page proof that machine M halts on input I. It then tries every one-page proof that machine M never halts on input I. Then it tries every two-page proof of each, and so on and so on.
It's quite plain that this wouldn't necessarily always work. By incompleteness, there are statements that can't be proven true or false; it makes sense that there might be Turing machines that are equivalent to these statements. The undecidability problem assures that indeed these do exist.
So, let's follow that through. [Begin standard proof.] We have built this function $f(a,b)$ to return $1$ if it finds a proof that program $a$ halts on input $b$, and $0$ if it finds a proof that $a$ doesn't halt. (We note that this function $f$ might never return, so it's not total computable.) We can make a function $g(a)$ that first calls $f(a,a)$, and returns $0$ if $f(a,a)=0$, and enters an infinite loop if $f(a,a)=1$.
If $f(g,g)$ terminated and returned 0, then $g(g)$ would terminate and return 0 -- but $f(g,g)$ terminating and returning 0 implies it found a proof of $g(g)$ not terminating, so this is impossible. If $f(g,g)$ terminated and returned 1, then $g(g)$ would never terminate -- but $f(g,g)$ returning 1 implies it found a proof of $g(g)$ terminating. [End standard proof.]
This pair of paradoxes is used in the standard proof to show that there is no function $f$ that always returns $0$ or $1$. There's no problem here, though, because we allow $f$ to not terminate -- and so indeed, it must never terminate, when given the inputs $g$ and $g$.
Here's where I'm confused. Because $f(g,g)$ never terminates, this implies that there is no disproof to be found, because it tries all of them. Suppose that $g(g)$ terminated at some point. Then by running simply it for that many steps, we can see that terminates, and this constitutes a perfectly valid proof.
Keep in mind that $f$ is a real program, and so is $g$. We know that for these concrete values (in some numbering system), $g(g)$ can't terminate, otherwise $f(g,g)$ would find the dumb proof of simply running it to that point.
The above constitutes a proof that $g(g)$ never terminates, and so the function $f(g,g)$ should find this proof, and use it to show that $g(g)$ doesn't terminate, but this is also a problem.
I'm sure there's something here I'm dramatically misunderstanding; I appreciate the time from anyone to answer.