I am not sure if this is a trivial question. By Post's theorem we know that every PA (first order logic) theorem is equivalent to stating that a given input C in a given Turing machine halts or doesn't halt. But it is not clear to me if that means that knowing all PA theorems (I mean, those wff. that are provable), is equivalent to knowing the halting problem for any halting problem that can be solved, that is those that in principle could be proved to either halt or not halt (this of course exclude those beyond the first Turing jump), regardless of the input and regardless of the specific Turing machine.
Question expansion after the answers: When I posted the question, I didn't have in mind any specific theory for proving if a Turing machine would or would not halt. In that sense T97778 was correct. But I had in mind a proof that gives you the correct (true) answer. It didn't need to be limited to PA. I now realize this way to think about it is either not precise, or either we can never be sure that a proof that a given TM halts is correct. Or is this incorrect? is there any formal system T that guarantees us that a proof in T that a machine halts or doesn't halt is true? By "true" I assume that there is a specific truth value for the halting problem, so there are no non-standard interpretations of a Turing machine. So for my question to make sense, it needs first to be answered (in the affirmative) the above question: is there any formal system T that guarantees us that a proof in T that a machine halts or doesn't halt is true? Does this question makes sense at all? (I guess that a system that assumes Con(PA) does not qualify, because not everybody agrees that PA is consistent, on the other hand, I do not want to restrict the proof to finitist ones).
New edit: I think you are right, the TM statement equivalent to the Paris Harrington theorem would what the machine does is to search for the least n, m, k, for which there is an N. The machine would halt if it finds such n, m, k. An oracle machine is able to use the oracle ∅′ to repeatedly test whether each triplet n, m, k is in the set and then halt if it finds a triplet that is not in the set. So the Paris Harrington (PH) conjecture is then equivalent to the claim that that machine does not halt when run with an oracle for ∅′. If it never halts, that means it never finds a triplet for which there is no N. the PH theorem shows that there is always such N for each triplet, so the machine doesn't halt (As you said). Am I correct? is that what you meant T9996725? If that is the case, then the answer to my original question would be a NO!!! the PH shows an example of a halting problem that we can solve (by solve I mean know if the TM is gonna stop or not), and that cannot be proved from PA (that is, is not a theorem of PA). Please somebody answer if this is correct.