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.
Best Answer
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