Imagine you have an oracle that can determine if an arbitrary statement is provable in Peano arithmetic. Then you can try using it as a halting oracle: for an arbitrary Turing machine T, ask "can PA prove that there's an integer N such that T makes N steps and then halts?". If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts. And if the oracle says no, you know that there's no such standard integer N because otherwise the oracle would've found a long and boring proof involving the encoding of N as SSS...S0, therefore T doesn't halt. So your oracle can indeed serve as a halting oracle.

I don't think this works. We can't expect PA to decide whether or not any given Turing machine halts. For example, there is a machine which enumerates the theorems proven by PA and halts if it ever encounters a proof of 0=1. By incompleteness, PA will not prove that that this machine halts. (I'm assuming PA is consistent.) This argument works for any stronger consistent theory as well, such as ZFC or even much stronger ones. Note: I basically stole this argument from Scott Aaronson.

Note that this is different from the question of whether or not the halting problem is reducible to the set of theorems of PA (i.e. whether or not the oracle you've specified is enough to compute whether or not a given TM halts). It's just that this particular approach does not give such an algorithm.

ETA: I was in error, see replies. In the OP, PA doesn't need to prove that a non-halting machine doesn't halt, it only needs to fail to prove that it halts (and it certainly does, if we believe PA is sound).