[GTP]

My memories of theoretical computer science are quite rusty, but I seem to see an issue with your argument: if you need enumeration you meet semidecidability. In other words, if you start generating the proofs and you find the one you were looking for, then problem solved. But if you can't find the proof, you would need to keep generating them at infinity to find the one you need. You can't conclude the result in this way without enumerating all possible proofs. Unless, you have a way of limiting the number of proofs that need to be generated?

[casercaramel144]

You are bounded by the fact that the statement is provable. Let a statement M be provable with a proof length K. By contradiction, if K is non finite, the statement must not be provable. Thus, there must be some positive integer K s.t. the proof length < K. Thus, it suffices to enumerate all proofs of length < K.

Insofar as we are given provability, we can solve halting.