I got a bit confused by a discussion about the provability of the Goldbach conjecture and the seemingly different opinions about this subject. Since I understand computer science better, I will ask my question related to the halting problem. Consider a universal Turing machine and the set of programs that can run on this machine. My first question is about the truth of the following statement:

- "For every computer program, there exists a proof in some consistent, recursively enumerable theory T that decides whether the computer program halts or runs forever."

Note that T may differ for every computer program that is considered. If this first statement is true, then I want to know about the truth of a second statement:

- "There exists a computer program that will halt according to some consistent r.e. theory $T_1$, and that will run forever according to some other consistent r.e. theory $T_2$."

If this second statement is true, could you then give an example?