# Is there a consistent theory for each instance of the halting problem?

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:

1. "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:

1. "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?

For statement (1), consider any fixed program $p$, to be run on input $0$. If $p$ actually halts on that input, then this will be provable in PA. If it doesn't, then the assertion "$p$ does not halt" is true and hence consistent with PA. So we could add that statement to PA and get a theory proving that $p$ does not halt.
Consider now statement (2). Notice that PA proves every true instance of halting. But it cannot be that PA, if consistent, proves every true instance of non-halting, since otherwise we would be able to solve the halting problem by looking for proofs. So there must be some program $p$ such that $p$ does not halt, but there is no proof of this in PA. Since it is true that $p$ does not halt, we may on the one hand add the assertion "$p$ does not halt" to PA to get a theory proving that $p$ does not halt. But on the other hand, since PA does not prove that $p$ does not halt, it means we can also add the assertion "$p$ halts" to PA and get a consistent extension of PA that proves that $p$ does halt. In other words, it is independent of PA whether $p$ halts, and this verifies (2).
• I guess, if you want to prove that the algorithm that solves the halting problem by looking at PA proofs actually solves the halting problem, you may want $\Sigma_1$-soundness of PA assumed in the metatheory you are proving this in? – Burak Nov 7 '14 at 17:59