# Is deciding whether a Turing machine *provably* runs forever equivalent to the halting problem?

Assume for this question that ZF set theory is sound.

Now consider the language "PROVELOOP," which consists of all descriptions of Turing machines M, for which there exists a ZF proof that M runs forever on a blank input.

It's clear that PROVELOOP is recursively-enumerable, and hence reducible to the halting problem. I can also prove that PROVELOOP is undecidable (details below). But I can't see how to prove that PROVELOOP is Turing-equivalent to the halting problem! (This is contrast to, say, the set of all descriptions of Turing machines that provably halt, which is just the same thing as the set of all descriptions of Turing machines that do halt!)

I'm guessing that there's a reduction from HALT that I haven't thought of, though it would be exciting if PROVELOOP were to have intermediate degree like the Friedberg-Muchnik languages. In any case, whatever the answer, I assume it must be known! Hence this question.

Proof that PROVELOOP is undecidable. Consider the following problem, which I'll call "Consistent Guessing" (CG). You're given as input a description of a Turing machine M. If M accepts given a blank input, then you need to accept, while if M rejects you need to reject. If M runs forever, then you can either accept or reject, but in either case you must halt.

By adapting the undecidability proof for HALT, we can easily show that CG is undecidable also. Namely, suppose P solves CG. Let Q take as input a Turing machine description $\langle M \rangle$, and solve CG for the machine $M(\langle M \rangle)$ by calling P as a subroutine. Then $Q(\langle Q \rangle)$ (i.e., Q run on its own description) must halt, accept if it rejects, and reject if it accepts.

Let's now prove that CG is Turing-reducible to PROVELOOP. Given a description of a Turing machine M for which we want to solve CG, simply create a new Turing machine M', which does the same thing as M except that if M accepts, then M' goes into an infinite loop instead. Then if M accepts, then M' loops, and moreover there's a ZF proof that M' loops. On the other hand, if M rejects, then M' also rejects, and there's no ZF proof that M' loops (by the assumption that ZF is sound). If M loops, then there might or might not be a ZF proof that M' loops -- but in any case, by calling PROVELOOP on M', we separate the case that M accepts from the case that M rejects, and therefore solve CG on M. So $CG \le_{T} PROVELOOP$, and PROVELOOP is undecidable as well.

One more note. In the comments of this blog post, Andy Drucker supplied a proof that CG is not equivalent to HALT, but rather has Friedberg-Muchnik-like intermediate status. So, the situation is

$0 \lt_{T} CG \le_{T} PROVELOOP \le_{T} HALT$

with at least one of the last two inequalities strict. Again, I'm sure this is all implicit in some computability paper from the 1960s or something, but I wouldn't know where to find it.

-
Note that GC is not a well-defined set and so $GC \leq_T PROVELOOP$ is not meaningful. There are many solutions to the separation problem, some of which are $<_T HALT$ while others are way up in the stratosphere. What you have shown is that PROVELOOP computes a separating set and is therefore not computable since the separation problem has no computable solution. In fact, it is known that if $X$ is a solution to the separation problem, then there is another solution $Y$ such that $0 <_T Y <_T X$. So there is a solution to the separation problem which is $<_T PROVELOOP$. – François G. Dorais May 22 '13 at 3:05
François: Yes, I know that CG is not a set; rather, it's what you call a separation problem and what complexity theorists would call a promise problem (the promise being that M halts). But the notion of Turing-reducibility can be generalized to promise problems in a fairly straightforward way, and once you do that $CG\le_T PROVELOOP$ becomes meaningful. Your last observation, implying that in fact $CG\lt_T PROVELOOP$, is quite interesting and not something I knew -- thanks for that! – Scott Aaronson May 22 '13 at 3:15
Ah, I guess your promise problems are what computability theorists call mass problems? – François G. Dorais May 22 '13 at 3:17

The first thing to notice is that if ZF is consistent, then it is consistent with ZFC that what you call ProveLoop is actually decidable. The reason is that if ZF is consistent, then by the incompleteness theorem, it is consistent with ZFC that $\neg$Con(ZF), in which case everything is provable in ZF, in which case every program is in ProveLoop.

So in the proof that ProveLoop is undecidable, one needs to make an additional assumption about the reliability of the proofs in ZF to avoid this issue with the incompleteness theorem.

Meanwhile, under such a consistency assumption, ProveLoop is indeed equivalent to the halting problem.

Theorem. Assume Con(ZF). Then ProveLoop is Turing equivalent to the Halting problem.

Proof. Under the Con(ZF) assumption, it follows that whenever ZF proves that a program doesn't halt, then it really doesn't halt, since if it did halt, then this fact would also be provable, contrary to consistency.

Clearly ProveLoop is c.e. and hence reducible to the halting problem, as you pointed out. Conversely, let's reduce the halting problem to ProveLoop. Given any program $p$, we want to decide whether $p$ halts on a blank tape, using an oracle for ProveLoop.

Define a computable function $f$, so that $f(q)$ is the program such that, on trivial input, if $p$ halts on the blank tape, then $f(q)$ jumps into an immediate infinite loop, and otherwise, while waiting for $p$ to halt, the program $f(q)$ halts just in case it finds a proof that $q$ does not halt. By the recursion theorem, there is a program $r$ such that $r$ and $f(r)$ compute the same function, and we can find this $r$ effectively. Furthermore, by using the $r$ from the proof of the recursion theorem, we may also assume that ZF proves that $r$ and $f(r)$ compute the same function. Notice that it can't ever be that $r$ halts on account of finding a proof that $r$ does not halt, by our assumption which ensures the accuracy of proofs of non-halting, and so definitely $r$ does not halt in any case. Meanwhile, if $p$ halts, then $r$ does not halt, but for a trivial reason that will be provable in ZF, namely, the fact that $p$ halted; and otherwise, when $p$ does not halt, then $r$ will run forever, but this fact will not be provable (for if it were provable, then $r$ would halt, contrary to consequence of our assumption that such proofs are reliable). So what we have is exactly a reduction of the halting problem to ProveLoop, as desired. QED

-
Thanks, Joel! Here's my simplification of your argument, avoiding the use of the recursion theorem. Given a TM M, construct a new TM M' that simulates M, but that while it runs, also (in parallel) searches for a proof in ZF that 0=1, and halts if it ever finds one. Meanwhile, if M ever halts, then M' terminates the 0=1 branch and simply runs forever. Then in any case M' runs forever. But if M halts then ZF proves that M' loops, while if M loops then ZF doesn't prove that M' loops (assuming ZF is consistent). So by running PROVEHALT on M', we also decide whether M halts, QED. – Scott Aaronson May 22 '13 at 4:38
However, notice that both my argument and yours only used the assumption that ZF is consistent, nothing more! Admittedly ZF doesn't prove that the reduction works, but ZF does prove the conditional result that the reduction works assuming Con(ZF). And I said at the outset that I was happy to assume even the soundness of ZF! – Scott Aaronson May 22 '13 at 4:43
Yes, that seems to work! I think it is a fun problem; the key was to find a program that in any case wouldn't halt, but would do so in a provable way when a given program halts, and not otherwise. What the arguments show is that the sets are not only Turing equivalent, but also $1$-equivalent, for we seem to have $1$-reductions both ways. So the two decision problems are computably isomorphic. – Joel David Hamkins May 22 '13 at 4:49

This is a complement to other answers, giving some "higher level" reasons why $PROVELOOP$ must be complete.

For a recursively enumerable set $A$, the following are equivalent:

1. $A$ is Turing complete (i.e. $A \equiv_T 0'$).
2. $A$ computes a fixed-point free (FPF) function (i.e. a total function $f$ such that $\varphi_e \neq \varphi_{f(e)}$ for all indices $e$).
3. $A$ computes a diaginally non-recursive (DNR) function (i.e. a total function $g$ such that if $\varphi_e(e)$ halts then $\varphi_e(e) \neq g(e)$).

The equivalence of (1) and (2) is the Arslanov Completeness Criterion and the equivalence with (3) was observed by Jockusch [Degrees of functions with no fixed points, in Logic, methodology and philosophy of science, VIII (Moscow, 1987), 191–201]. Conditions (2) and (3) are very useful tests for completeness of recursively enumerable sets.

A variation of Scott's $CG$ argument shows that $PROVELOOP$ computes a separating function for the disjoint recursively enumerable sets $$A_0 = \lbrace e : \varphi_e(e){\downarrow} = 0\rbrace, \qquad A_1 = \lbrace e : \varphi_e(e){\downarrow} = 1\rbrace.$$ That is $PROVELOOP$ computes a $\lbrace0,1\rbrace$-valued function $h$ such that $h(e) = 0$ if $e \in A_0$ and $h(e)= 1$ if $e \in A_1$. Then $g(e) = 1-h(e)$ is easily seen to be DNR. Since $g \leq_T h \leq_T PROVELOOP$ and $PROVELOOP$ is recursively enumerable, it follows that $PROVELOOP$ is complete.

-

It's late, so I might be making a mistake or several, but I think this works:

Assuming $ZF$ is consistent (I don't think soundness is necessary for this part), I'll show PROVELOOP can compute the set of $\Pi^0_1$ theorems of $ZF$.

Given a $\Pi^0_1$ sentence in the language of set theory $\varphi$, build in the usual way a machine $M$ which runs until it finds a counterexample to $\varphi$; $M$ provably loops iff $ZF$ proves $\varphi$. In one direction, if $ZF$ proves $\varphi$, then $M$ has to loop forever since $ZF$ is consistent; and what's more, as long as the construction of $M$ was sufficiently transparent, $ZF$ can prove this, so $\ulcorner M\urcorner\in PROVELOOP$. In the other direction, if $ZF$ proves $\neg\varphi$, then $ZF$ proves that $M$ halts; if $ZF$ is consistent, then that means $ZF$ does not prove that $M$ does not halt, so $\ulcorner M\urcorner\not\in PROVELOOP$.

Now, all I need to do is show that the set of $\Pi^0_1$ theorems of $ZF$ is equivalent to the halting problem, $H$. For some reason I'm having trouble doing this at the moment, but I think this is straightforward (can someone fill this gap?). I think it's in this second step that Soundness (or $\Sigma_1$-Soundness) will be necessary.

-
Thanks, Noah! But yes, that second step was precisely the one that I couldn't see how to do. – Scott Aaronson May 22 '13 at 3:07
My argument reduces the question of whether $p$ halts or not to the question of whether or not it is provable that $r$ runs forever, which is a $\Pi^0_1$ assertion. So under the $\Sigma_1$-soundness assumption, this establishes that indeed the halting problem is Turing equivalent to the set of provable $\Pi^0_1$-assertions, just as you had claimed. – Joel David Hamkins May 22 '13 at 3:55
I guess my argument used Con(ZF) rather than $\Sigma_1$-soundness. – Joel David Hamkins May 22 '13 at 4:12