Q1: Yes (except that the certificates you get may have size polylogarithmic in $n$, not just logarithmic, and you need to apply the argument to both HALTS-IN-N and its complement, as pointed out by Andreas).
Q2: Well, NP = EXP contradicts all kinds of conjectures from complexity theory: it makes the polynomial hierarchy collapse to NP = coNP, it makes NP = PSPACE, and PSPACE = EXP, all of which are assumed to be false. On the other hand, it also implies P ≠ NP. We cannot rule out NP = EXP with the present state of knowledge (nor the even stronger collapse ZPP = EXP), but the time hierarchy theorem implies that $\mathrm P\ne\mathrm{EXP}$ and $\mathrm{NP}\ne\mathrm{NEXP}\cap\mathrm{coNEXP}$. Existence of succinct certificates also shows up in other similar situations: for example, if EXP has polynomial-size Boolean circuits, then membership in any EXP language has succinct certificates verifiable in randomized polynomial time (that is, EXP = MA).
Vis-à-vis the last but one paragraph of your question, note that an exhaustive deterministic search for a short certificate takes time exponential in the size of the certificate, so you don’t save here anything in terms of deterministic running time.
I don’t follow the last paragraph. EXP = NP implies $\mathrm{DTIME}(2^{t(n)})\subseteq\mathrm{NTIME}\bigl(t(n)^{O(1)}\bigr)$ for every time-constructible function $t(n)$ of at least polynomial growth, if that’s what you mean, but this does not lead to a contradiction.
EDIT: It may be worth mentioning that there is nothing particularly revolting about the idea that the existence of an exponentially long computation can be proved using a polynomial amount of data. In fact, Babai, Fortnow, and Lund have shown that NEXP = MIP, which means that two (computationally unlimited) agents presenting polynomial-size evidence who cannot communicate with each other can reliably convince a randomized polynomial-time verifier that such an exponentially long halting computation (even nondeterministic) exists. (Here, polynomial and exponential is measured in terms of the length of the input, which is logarithmic in the $n$ from the original question.)
EDIT 2: Yes, the running times for primitive recursive functions (or predicates) are enormous. More precisely, a function is primitive recursive if and only if it is computable in time $A(k,n)$ for some constant $k$, where $A$ is the Ackermann function. Plugging an extra exponential or logarithm in this characterization makes no difference. In view of the latter fact, whether NP = EXP or not has not much to do with the argument: we know unconditionally that the version of HALTS-IN-N where $n$ is given in unary is in P.
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
Best Answer
Yes, for starters there is the arithmetical hierarchy, where enumerable = $\Sigma^0_1$ and it continues $\Pi^0_1$, $\Delta^0_2$, $\Sigma^0_2$ etc.
See also the Computability Menagerie.