# How to formalize “Is there a proof for every instance of the halting problem?”? [closed]

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?

## closed as primarily opinion-based by user9072, Stefan Kohl, Emil Jeřábek, Goldstern, S. Carnahan♦Nov 10 '14 at 0:47

Many good questions generate some degree of opinion based on expert experience, but answers to this question will tend to be almost entirely based on opinions, rather than facts, references, or specific expertise. If this question can be reworded to fit the rules in the help center, please edit the question.

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$.
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$.
• 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... – მამუკა ჯიბლაძე Nov 14 '14 at 19:01
• @მამუკაჯიბლაძე 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. – Joel David Hamkins Nov 14 '14 at 19:33