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

Question

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.

Answer 1

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.

Answer 2

If you want to do a proof by contradiction, you have to structure the proof like this. (1) assume the thing, (2) derive some conclusion (3) the conclusion is logically inconsistent, so the assumption is false. Q.E.D! $\square$ In this case: suppose that the Halting Problem is decidable. Then there is a Turing Machine $H$ which computes it. Then I can define another Turing Machine with logically inconsistent behaviour: it calls $M$ and halts iff it says I loop forever, and otherwise, if it says I'm ok, then I go and enter an infinite loop. So any supposed answer errs on at least one instance. Therefore the Halting Problem is not decidable.

All proofs by contradiction follow this scheme. The mistake you made was to omit step (1), where you have to assume that the Halting Problem is decidable. You say, we note that this function $f$ might never return, so it's not total computable. Well, if $f$ is not required even to halt, it isn't required to do anything! In your formulation, you assume that the Halting Problem is semi-decidable, which is true. A language is semi-decidable if there is a Turing Machine which halts on all yes instances but not on all no instances.

Now for something else. Take a set of axioms: ZFC, Peano Arithmetic or your personal favorite. It is a finite list of axioms, and a finite list of rules that infer from these axioms. So go and do that: Let $M$ be a Turing Machine that, when given the empty tape, writes down the axioms, then makes all the one-step inferences, then writes down all the two-step proofs, and so forth. With each proof, it checks for a contradiction: Have I proved $p\wedge\neg p$? When it finds a contradiction, it halts.

$M$ May halt or not, but whatever the case, you cannot prove it in the same system you started with because if you could, then ZFC could prove its own consistency, but we know that it can't! Scott Aaronson has a nice entry on this on his blog (link). This is an explicit TM with $7,918$ states whose halting behaviour is not provable within a particular axiomatic setting.

This means it's not provable within ZFC, or Peano arithmetic, which is quite different from what you are trying to do, which is to establish unconditionally that there is no TM which always outputs the right answer.