1
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
10
$\begingroup$

Both statements are true.

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).

Improve this answer
$\endgroup$
6
  • $\begingroup$ 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? $\endgroup$
    – Burak
    Commented Nov 7, 2014 at 17:59
  • $\begingroup$ Yes, I agree with that. $\endgroup$
    – Joel David Hamkins
    Commented Nov 7, 2014 at 19:02
  • $\begingroup$ Ok, I see. The reason why this is so disappointingly simple is because these consistent theories will not be sound? Should I restate the question for 'sound' theories, instead of consistent, to get more interesting answers? $\endgroup$
    – Ward Blondé
    Commented Nov 7, 2014 at 23:07
  • $\begingroup$ Well, you can't have it for sound theories of any strength, since if one of the theories proves the program halts, then by soundness it must really halt, in which case the other theory will also prove that. $\endgroup$
    – Joel David Hamkins
    Commented Nov 7, 2014 at 23:32
  • $\begingroup$ So question 2 would be false for sound theories. But what about question 1? $\endgroup$
    – Ward Blondé
    Commented Nov 7, 2014 at 23:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .