0
$\begingroup$

In a previous question that I asked here it turned out that for every instance of the halting problem, being the matter whether a certain computer program halts or runs forever, there exists a consistent theory that decides and proves this instance. It also turns out there exists a sound theory that decides and proves this instance. For example, consider the program that checks the Goldbach conjecture and halts when it finds a counterexample. If this program never halts, then a proof for it exists in the theory that consists of the Peano Arithmetic axioms plus the axiom "The Goldbach checking program never halts". This theory trivially proves the non-halting of the Goldbach checking instance, but the problem is that mathematicians would not have trust in the soundness of this theory, even though the theory may very well be sound and consistent. For this reason I will make a new attempt to formalize my question:

Is there a proof and a theory for every instance of the halting problem, in such a way that the proofs and the theories that arise would be accepted by arbitrarily large and complex theorem provers as being correct proofs in a sound theory?

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
7
$\begingroup$

Let $TA$ be the theory of true arithmetic, that is, the set of all truths of the usual standard model of arithmetic $\langle\mathbb{N},+,\cdot,0,1,<\rangle$. It is a theorem of ZFC that TA is consistent and sound for arithmetic truth, since for a theory to be sound means precisely that it agrees with $TA$.

Meanwhile, the theory TA proves all and only the true instances of halting and non-halting, so every instance of the halting problem or indeed any arithmetic question is correctly settled by the theory TA, by definition.

Probably you don't find this answer satisfactory, because we can't so easily tell what are the axioms of TA. But in this case, my response is that there will be no satisfactory answer for you. There can be no assignment of every instance $p$ of the halting problem to a sound consistent theory $T_p$ that settles the question of whether $p$ halts or not. The reason is that if we could compute this map $p\mapsto T_p$, then we could solve the halting problem: on input $p$, start enumerating all proofs in the theory $T_p$ until you find one that solves the issue of whether $p$ halts or not. It will be correct, by soundness, and so you will have solved the halting problem.

We can't even have a computable procedure by which from $p$ we can gradually enumerate the axioms of $T_p$, since from any such procedure we can still enumerate all proofs from $T_p$.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Thanks! The answer on my question is 'no' (for clarity) and I am certainly not unsatisfied with this. Instead, I was unsatisfied with the most popular answer of Terry Tao here, which makes use of exotic numbers, as well as some comments there that refute the doubt of Knuth. This made me have the impression that mathematicians have a way to bypass the negative results of Gödel and the halting problem. $\endgroup$
    – Ward Blondé
    Commented Nov 10, 2014 at 11:09
  • $\begingroup$ Does this rule out that for each given $p$ there is a $T_p$ which can be described effectively in some rigorous sense? If I am not mistaken, $TA$ cannot be effectively described in any sense... $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Nov 14, 2014 at 19:01
  • 1
    $\begingroup$ @მამუკაჯიბლაძე No, my answer at the other question (mathoverflow.net/a/186498/1946) shows that for any give $p$, there is a c.e. sound theory $T_p$ that correctly settles whether $p$ halts or not. This answer here shows that we cannot computably go from $p$ to that theory $T_p$. But meanwhile, the noncomputable consistent sound theory TA always works. $\endgroup$
    – Joel David Hamkins
    Commented Nov 14, 2014 at 19:33

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