Is there an equivalence between "does this program halt" and "is this sentence provable"?
If a Turing machine halts on a given input, then you can prove this in any reasonable propositional proof system. The idea is to list the halting sequence of configurations of the Turing machine, and prove, one by one, that these are the configurations encountered by the Turing machine when run on the given input.

In the other direction, if a sentence is provable in a reasonable proof system, then the Turing machine which goes over all proofs in the system and checks whether they prove the sentence, will halt, and its halting implies that the sentence is indeed provable in the proof system.

What this shows is that Turing machines with an oracle for the halting problem have the same power as Turing machines with a provability oracle for any reasonable proof system.