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.

Answer 3

It makes no sense because it falls. That is, the traditional breaker to the halting problem is an error of logic and not an actual disproof. As reference Ricky Demer's statement, it ends up not proving ZFC is inconsistent but that the original statement is paradoxical. Suffice it to say that if this were the only reason, we would be able to prove the matter for all non-self-referential cases and throw on all self-referential cases which would be good enough for all reasons we want to solve the halting problem.

I am in possession of a theorem that reads "There exists a set of laws of physics that admit the construction of a hyper computer that can solve the halting problem for the Turing machine, and in turn the Turing machine can solve its halting problem."

If we begin by positing the ability to construct the relativistic spacetime with the property of having infinite inverse time dilation but finite space contraction and finite blueshift we can place a Turing machine within. I once had in my hand a paper that described such a solution to general relativity and considered certain hyper-computer problems within but not the halting problem. If we admit that such a thing could exist in designer laws of physics I need make no more references to the paper I can no longer find.

The laws of physics demanded to construct the anomaly in turn always involves nasty beasts where inverse time dilation is available, and time travel would be available if the laws are anything like our own.

If we consider running a Turing machine in there and signaling by radio on halting, if we get a signal we know the machine halts. Barring breakdown (which we exclude in theory) we therefore know if we get no signal the Turing machine in question does not halt. Due to the infinite time dilation we need wait a finite time only. The downside of the time dilation is while we can receive a signal, we cannot decode it as it is arbitrarily fast. But the mere presence or absence is one bit, and that's all we need.

We may now construct the following machine: The machine accepts a Turing machine descriptor as input, constructs the spacetime anomaly described above with such a Turing machine as described on its tape within, and waits a certain amount of time for an answer (it knows exactly how long because it constructed the spacetime). Obviously this machine halts.

My theorem in turn forces 4-state logic to appear out of nowhere because it must be possible to represent the truth-value of such a beast as the self-halting-test involved, and the truth value is "inconsistent" or "paradox" depending on how you want to define it. (The remaining truth value is "independent"; that is our axioms cannot prove it either true or false at all, like C is to ZF).

We may construct a 4-state reasoning machine that can classify all statements (P) into their four categories as follows: Given a breadth-first theorem solver (the proof of existence is trivial), run A = halts(bredth-first-theorem-solver(P)) and B = halts(bredth-first-theorem-solver(!P)).

If A and not B then P is "true"
If not A and B then P is "false"
If A and B then P is "inconsistent"
If not A and not B then P is "independent" (of axioms)