Does every instance of the Halting Problem have a proof of acceptance or rejection?

Question

I know that the Halting Problem $HALT = $ {$⟨M,w⟩$ | TM $M$ halts on input $w$} is undecidable, but that it is trivially decidable for each instance of the problem $⟨M,w⟩$ (with the decider being the TM that always rejects or accepts). My question is that does this mean there is a proof (in some formal system) for every specific given instance of the Halting Problem $⟨M,w⟩$ with the proof either concluding that the $⟨M,w⟩ \in HALT$ or $⟨M,w⟩ \notin HALT$ ?

My first thought is no because that would mean a potential halting decider could iterate over all proofs then stop once we've found the positive or negative one, but it feels intuitively wrong to say "its not possible to explain why this particular program loops". What am I missing?

Answer 1

The Gödel sentence of an axiom system $T$ is of the form $\forall n R(n)$, where $R$ is a recursive predicate. Hence, the halting problem of the algorithm that goes through natural numbers to find $n$ such that $R(n)$ is false is not provable.

It is easy to see that this means also that the Gödel sentence is true, but it is not provable in $T$.

• messed: Thank you for your response. My follow up question would be that is it fair to say that we can still "determine" the halting or looping behaviour of any specific instance if we are not restricted to that axiom system? For example you just determined that the sentence you mentioned is true, which means you determined that program would loop, right?
• Command Master: @messed it all depends on what axioms you accept. For example in true arithmetic (an axiom system consisting of all true arithmetic statements) you can prove whether any particular program halts or doesn't. However, you can't check proofs in this system — you don't know if something is truly an axiom. Gödel's incompleteness theorem means that if you can compute the axioms of the system there are necessarily some programs it doesn't decide
• Mikko Pitkonen: Of course there are some assumptions in the Gödel's incompleteness theorem, which I forgot to put there. If the program halts, then naturally we can prove that, but if the program doesn't halt, we can't prove that in $T$ which satisfies the conditions of the Gödel's incompleteness theorem. If we know that the statement $\forall n R(n)$ is independent, we know it is true, but we might not know it.
• messed: @CommandMaster by "check proofs" do you mean I can't validate a potential proof, or that I cannot enumerate all proofs? Thanks.
• Noah Schweber: @CommandMaster That's very false. The set of all valid proofs in true arithmetic is much worse than r.e. - it's not even in the arithmetical hierarchy. See Tarski's undefinability theorem. Indeed, by Craig's trick an r.e. proof system is no worse than a recursive proof system.