Is the set of PA theorems the same as the set of solvable halting problems?

Question

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.

Answer 1

The answer to the question is NO. The Paris Harrington theorem 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), but was demonstrated to be true using a theory stronger that PA.

Answer 2

The set of '[turing machines] that in principle could be proved to either halt or not halt' is not a well-defined concept, because the notion of proof depends in an arbitrary way on the formal system you choose. For instance in an inconsistent system every Turing machine provably halts and dont halts. Or if you want to keep consistency, create two new systems, add the axiom 'T_k halts' to one and 'T_k does not halt' to the other. So every Turing machine provably halts and dont halt.

Answer 3

By the standard encoding schemes one should be able to encode the halting of a given universal turing machine into PA. First encode the state of the Turing Machine as (a) a natural number representing the tape, and (b) a natural number representing the state of the machine, then pair these two values into a single integer. Since each step of the TM is finite, the tape state can always be encoded as a (possibly arbitrarily long) finite number; similarly, not just the state of the TM but the entire operation of the TM can easily be encoded in $\mathbb{N}$, using the standard coding techniques for representing finite collections of naturals as naturals. This lets you define a $\Delta_0$ function $f$ such that if $s$ represents a given (TM state, tape state) pair, then $f(s)$ represents the state of the machine and tape after one execution cycle. Similarly, since 'the machine has halted' is just 'the machine is presently in a halt state', that's easily encoded as a $\Delta_0$ predicate $g(s)$. With this in place, you can use the recursion theorem to encode the concept of '$x$ codes a (finite) sequence with a given $x_0$ such that $\forall i\lt \text{len}(x)$, $x_{i+1}=f(x_i)$ and $g(x_{\text{len}(x)})$' as a function $h(x, x_0)$. The halting of the machine on a given some input $x_0$ is then equivalent to the statement $\exists x h(x,x_0)$.

Answer 4

Every halting turing machine can be proved to halt in PA, as per Steven's answer, I dont know if every proof that a turing macine halts in PA is correct, (and I hope someone else answers this), but if it halts, then there is also a proof in PA of the type one can in theory recognize is true for a physical turing machine because the proof basically simulates every step of the turing machine until it halts.

No consistent theory can prove the non-halting in general because it would prove its own consistensy and thus be inconsistent. Alot of systems have only correct proofs of non-halting, for instance the system whose only axiom is that a TM moving right every step doesnt halt.

Latest edit: Youre right, and Con(PA) is another example, which you have to assume for the PHT anyways.