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.


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.

  • 2
    $\begingroup$ The OP has already mentioned that they're talking about Peano Arithmetic, so you don't have the freedom to add arbitrary axioms. $\endgroup$ – Steven Stadnicki Feb 2 '13 at 18:02

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)$.

  • $\begingroup$ So, I guess my question was trivial and the answer to it is yes? is this equivalent to state that every statement independent of PA will encode a halting problem whose solution will never be known? $\endgroup$ – Wolphram jonny Feb 3 '13 at 2:52
  • $\begingroup$ Totally false. Steven misunderstand your qustion and confusion. Read my answer. What can be known depends as I say on what you mean by proof and know, since Godel these concepts dont admit any rigid mathematical definition. $\endgroup$ – user59761 Feb 3 '13 at 3:03
  • $\begingroup$ There is no theorem that says that PA contains all the reasonable proof-techniques, for instance the statement Con(PA) encodes a Turing machine that halts iff PA is inconsistent. Most mathematicians would say that PA is consistent, but you cant prove this in PA, thus you cant prove the non-halting of this machine in PA. $\endgroup$ – user59761 Feb 3 '13 at 3:12
  • $\begingroup$ @julianfernandez I would have said instead that the answer to your question is a non-trivial yes; the recursion theorem is far from trivial and its use to simulate the execution of a TM via a sequence of integers (and thus to simulate a halting run of a given TM by a single integer) is decidedly non-trivial. But not every statement of PA encodes a halting problem; I think it would be more correct to say that every statement of PA independent of the theory is encoded by a TM whose halting problem is unsolvable (within PA). $\endgroup$ – Steven Stadnicki Feb 3 '13 at 6:33
  • $\begingroup$ @T97778 It's true that there are ways of proving things other than PA, but the original question asked specifically about PA, not about other theories. There is a perfectly rigid definition of 'proof within PA' or of 'proof within formal system T' for any formal system T; Godel's theorem does nothing to change the nature of provability, merely shows that it's not sufficient to capture the wholly different notion of truth. $\endgroup$ – Steven Stadnicki Feb 3 '13 at 6:34

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.

  • $\begingroup$ Yes, every proof in PA is correct, because the standard model is a model of PA. $\endgroup$ – Carl Mummert Feb 5 '13 at 12:32
  • $\begingroup$ but there are also proofs in PA that some machine doesn't halt. Can we be sure that indeed it will never halt? and regarding systems stronger than PA, such as PA+ Paris Harrington theorem. Doesn't it prove that a certain machine halts? can we be sure that that machine will actually halt? $\endgroup$ – Wolphram jonny Feb 6 '13 at 1:48
  • $\begingroup$ and any theory T that has N as a model prove things that are true? $\endgroup$ – Wolphram jonny Feb 6 '13 at 1:52
  • $\begingroup$ 1) Yes, because PA is consistent 2) It proves that a certain TM does not halt 3) Yes $\endgroup$ – user61072 Feb 6 '13 at 14:40
  • $\begingroup$ Acording to wikipedia: "The smallest number N that satisfies the strengthened finite Ramsey theorem is a computable function of n, m, k, but grows extremely fast. In particular it is not primitive recursive... Its growth is so large that Peano arithmetic cannot prove it is defined everywhere". Would not that mean that the machine does indeed halt in finite time? (only that you cannot prove it in PA) $\endgroup$ – Wolphram jonny Feb 7 '13 at 4:54

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.