Undecidability instance on a "find a proof/disproof" machine

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 tha

So $f(M,I)$ is this machine that "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"...

That's fine, but later on you say "The above constitutes a proof that $g(g)$ never terminates, and so the function $f(g,g)$ should find this proof."

That is not true, since you didn't write that proof as a formal proof in terms of "ZFC, let's say, or Peano arithmetic, or whatever", so there is no reason to expect $f(g,g)$ to find it. You didn't even define $f(a,b)$ of $g(x)$ in terms that would translate into most such formal systems.

You assume that you would be able to specify a real formal system if you had to, with sufficient power to express $f$ and $g$ in concrete terms and prove what you say about them, but Godel's theorem says that's not necessarily so.

Furthermore, you say that $f$ and $g$ are real programs, but that is not true until this formal system is specified. Because of this you have not proven what you set out to prove. What you have proven is Godel's theorem -- any formal system that allows you to express your claim in terms of itself will either be inconsistent, or will not contain your proof.

StackExchange Computer Science Q#24790, answer score: 3