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, but I wouldn't know where to find it.

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.

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!

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, but I wouldn't know where to find it.

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, but I wouldn't know where to find it.